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

The Invariant Checker: Automated Deduction Verification of Reactive Systems
 by Dr. Hassen Saïdi.

Abstract
The Invariant Checker is a tool for the computer aided verification, dedicated, dedicated to the proof of invariance properties of reactive systems. The aim of the tool is to provide a framework combining theorem-proving techniques (Pvs theorem prover) and deductive verification methods. Systems are described as a parallel composition of sequential programs described in a language close to the Dijkstra guarded command language. Program variables can be of any type definable in Pvs. The tool provides automatic generation od invariants, automatic strengthening od invariants and automatic abstarction. The tool is interfaced with ALDÉBARAN, a tool for the analysis of state graphs
Files
 













 

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