Hector: Software Model Checking with Cooperating Analysis Plugins

We present Hector, a software tool for combining different abstraction methods to extract sound models of heap-manipulating imperative programs with recursion. Extracted models may be explored visually and model checked with a wide range of “propositional” temporal logic safety properties, where “propositions” are formulae of a first order logic with transitive closure and arithmetic (L). Hector uses techniques d in [4, 5] to wrap up different abstraction methods as modular analysis plugins, and to exchange information about program state between plugins through formulae of L. This approach aims to achieve both (apparently conflicting) advantages of increased precision and modularity. When checking safety properties containing non-independent “propositions”, our model checking algorithm gives greater precision than a na¨ıve three-valued one since it maintains some dependencies.

• Type: Conference
• Year: 2007
• Where: CAV
• Authors: Nathaniel Charlton, Michael Huth
• Keywords: CAV 2007, Different Abstraction Methods, Formal Methods, Logic Safety Properties, Safety Properties