Verifying invariants using theorem proving

Abstract

Our goal is to use a theorem prover in order to verify invariance properties of distributed systems in a “model checking like” manner. A system S is described by 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 S, we try to compute, in a model checking like manner, the weakest 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 an invariant 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 these predicates, we use either automatic or assisted theorem proving depending on their nature. We show in this paper how this can be done in an efficient way using the Prototype Verification System PVS. A tool implementing this verification method is presented.