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

PVS: Combining Specification, Proof Checking and Model Checking
 by Dr. Natarajan Shankar.

PVS is an automated tool for specification and verification that is designed to exploit the synergies between language and deduction, automation and interaction, and theorem proving and model checking. PVS strives for a balance between automation and interaction by using decision procedures to simplify the tedious and obvious steps in a proof leaving the user to interactively supply the high-level steps in a verification. Decision procedures for BDD-based propositional simplification and model checking, equality, and linear arithmetic are integrated into PVS. The utility of the language and deductive features of PVS have been demonstrated in a number of examples, including the specification and partial verification of the Rockwell-Collins AAMP5 processor design [9], and the verification of an SRT divider [13]. This tutorial concentrates on the integration of individual verification techniques available in PVS.


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