Verifying Invariants More Automatically

Vlad Rusu, Elena Zinovieva, and Duncan Clarke

to appear in Verification and Computational Logic, VCL'02


We present an algorithm that, given a transition system S and a set of 
auxiliary invariants A already proved on S, checks if a  predicate I is
inductive on S in the context of the auxiliary invariants. The answer 
is either yes, in which case I is an invariant of S, or don't know. The
algorithm accepts infinite-state systems with unbounded counters and 
parametric-size arrays, and predicates with quantifiers over unbounded
domains. As an example we verify  a component of an electronic purse 
system. By using our algorithm together with the PVS theorem prover the
verification is more automatic than that performed using PVS alone.

Contents: 

appendix.ps:  Appendix showing in detail what the algorithm does when 
              applied to the case study described in the (following) paper.

paper.ps:     The paper

query.dmp:    PVS version of the case study. To replay the proofs: save the
              query.dmp file in a directory DIR. Then, launch PVS 2.4. 
              Type ESC-x undump-pvs-files then load the requirements.pvs file 
              in your main emacs window, and type ESC-x prove-importchain.