Automated deductive verification of reactive systems

Abstract

The verification problem is one of deciding if a program M satisfies a given property P. The algorithmic or model checking approach to verification uses state-space exploration to demonstrate M |= P, so that the transition system given by the program is shown to be a model satisfying the property. The deductive approach proves an implication |- M \supset P between the logical formula representing the program and the formula representing the property. On an another hand, it is now widely accepted that abstraction techniques are useful and even necessary for a successful verification. Algorithmic methods are effective for finite-state systems of manageable size. Deductive methods are general but require considerable manual guidance, particularly in the choice of invariants. We show that is possible to combine algorithmic and deductive methods so as to increase the scope of the former while augmenting the automation of the latter. In particular, we show how a uniform technique based on abstract interpretation can be used to construct finite-state abstractions of infinite-state systems as well as to generate a certain class of invariance properties.

I will show how a combination of proof rules, invariant generation by static analysis and abstraction techniques integrated to a theorem prover can be used effectively to prove properties of systems given as a parallel composition of sequential processes with infinite data types. I will focus on the use of decision procedures to generate finite-state abstractions of infinite state systems. Finally, I will present an implementation of these various techniques in a tool built on the top of the PVS verification system developed at SRI.