SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
  SRI Logo

Automated Deductive Verification of Parallel Systems
 by Dr. Hassen Sa´di.

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.


About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2024 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy