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

Construction of abstract state graphs with PVS
 by Dr. Hassen Sadi & Sussane Graf.

In this paper. we propose a method for the automatic construction of an abstract state graph of an arbitrary system using the PVS theorem prover. Given a parallel composition of sequential processes and a partition of the state space induced by predicates φ1....,φi on the program variables which defines an abstract state space. we construct an abstract state graph, starting in the abstract initial state. The possible successors of a state are computed using the PVS theorem prover by verifying for each index i if φi or φi is a postcondition of it. This allows an abstract state space exploration for arbitrary programs.


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