Invisible invariants and abstract interpretation

Abstract

The method of Invisible Invariants provides a way to verify safety properties of infinite parameterized classes of finite-state systems using finite-state model checking techniques. This paper looks at invisible invariants from the point of view of abstract interpretation. Viewed in this way, the method suggests a generic strategy for computing abstract fixed points in the case where the best abstract transformer has a high computational cost. This strategy requires only that we can reasonably segregate the infinite concrete state space into finite subsets of increasing size or complexity. We observe that in domains for which the computation of the best abstract transformer may require an exponential number of calls to a theorem prover, we can sometimes reduce the number of theorem prover calls to just one, without sacrificing accuracy. © 2011 Springer-Verlag Berlin Heidelberg.