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.