@inproceedings{GS96,
title = { Verifying invariants using theorem proving },
author = {Graf, Susanne and Saidi, Hassen},
month = {jul},
year = {1996},
booktitle = {Conference on Computer Aided Verification CAV'96},
series = {LNCS},
volume = {1102},
team = {DCS},
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 <i>S</i> is described by a set of sequential components, each one given by a transition relation and a predicate <i>Init</i> defining the set of initial states. In order to verify that <i>P</i> is an invariant of <i>S</i>, we try to compute, in a model checking like manner, the weakest predicate <i>P'</i> stronger than <i>P</i> and weaker than <i>Init</i> which is an <i>inductive</i> invariant, that is, whenever <i>P'</i> is true in some state, then <i>P'</i> remains true after the execution of any possible transition. The fact that <i>P</i> is an invariant can be expressed by a set of predicates (having no more quantifiers than <i>P</i>) 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.},
}
