Abstraction and Compositionality for the Verification of Infinite-State Reactive Systems
Zohar Manna, Henny B. Sipma · 2001
We describe several techniques for verifying infinite-state systems via finite-state abstractions. Diagrams are top-down property-driven abstractions, which are especially suited for compositional, assume-guarantee reasoning. Predicate abstraction uses a bottom-up approach for generating abstractions; invariant generation techniques are applied to automatically generate the required predicates. Extended finite-state abstractions allow inclusion of extra information produced by the deductive abstraction, which can be used by the model checker to reduce the number of spurious counterexamples. These methods have been or currently are being implemented in the Stanford Temporal Prover. The methods have been applied in the analysis of a medical device.