This paper describes the use of deductive methods for the verification of invariance properties of parallel systems. We show how a combination of proof rules, invariant generation techniques and abstraction techniques integrated to a theorem prover can be used effectively to prove invariants of systems given as a parallel composition of sequential processes with infinite data types. We present an implementation of these various techniques in our tool the Invariant-Checker. The Invariant-Checker is build as a front-end for the PVS theorem prover. The tool is an extension of the PVS specification language to handle the notion of transition systems describing the parallel composition of sequential processes. The PVS prover is also extended with a new proof scheme corresponding to the combination of our proof techniques.

• lfm97-saidi.ps