Abstract and model check while you prove

Abstract

The construction of abstractions is essential for reducing large or infinite state systems to small or finite state systems. Boolean abstractions, where boolean variables replace concrete predicates, are an important class that subsume several abstraction schemes. We show how boolean abstractions can be constructed simply, effciently, and pre- cisely for infinite state systems while preserving properties in the full μ-calculus. We also propose an automatic refinement algorithm which refines the abstraction until the property is verified or a counterexample is found. Our algorithm is implemented as a proof rule in the PVS veri- fication system. With the abstraction proof rule, proof strategies combi- ning deductive proof construction, model checking, and abstraction can be defined entirely within the PVS framework.