Hector: Software model checking with cooperating analysis plugins

Abstract

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 (ℒ). HECTOR uses techniques initiated 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 ℒ. 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. © Springer-Verlag Berlin Heidelberg 2007.