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.

Abstract
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.
Files
 













 

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