Suzanne Graf and Hassen Saïdi
Verifying Invariants Using Theorem Proving
In Proceedings of 8th Computer-Aided Verification, July 1996, New Brunswick, NJ. LNCS, Springer-Verlag.
Abstract
We are interested in using a theorem prover in order to verify invariance properties of systems in a systematic ``model checking like'' manner. A system is described as a set of sequential components, each one given by a transition relation and a predicate Init defining the set of initial states. In order to verify that P is an invariant of system S, we try to compute, in an iterative model checking like manner, a predicate P' stronger than P and weaker than Init which is an inductive invariant, that is, whenever P' is true in some state , then P' remains true after the execution of any possible transition. The fact that P' is inductive can be expressed by a set of predicates (having no more quantifiers than P) on the set of program variables, one for every possible transition of the system. In order to prove that P' is inductive, we use either automatic or assisted theorem proving depending on the nature of the formulas to prove. We show in this paper how this can be done in an efficient way. The prover we use is the Prototype Verification System PVS. A tool implementing this verification method is presented.