Partial completeness of abstract fixpoint checking (invited paper)

Abstract

Interpretation is used in program static analysis and model checking to cope with infinite state spaces and/or with computer resource limitations. One common problem is to check abstract fixpoints for specifications. The abstraction is partially complete when the checking algorithm is exact in that, if the algorithm ever terminates, its answer is always affirmative for correct specifications. We characterize partially complete abstractions for various abstract fixpoint checking algorithms, including new ones, and show that the computation of complete abstract domains is essentially equivalent to invariance proofs that is to concrete fixpoint checking.