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

FME '96 Tutorial: An Introduction to Some Advanced Capabilities of PVS
 by Sam Owre & Dr. John Rushby.

Abstract
The specification language of PVS builds on classical higher-order logic and the simple theory of types. PVS extends simple type theory with dependent types and predicate subtypes, structures specifications into parameterized theories, and adds a construction for freely generated abstract data types. These extensions provide a surprisingly rich set of capabilities, and the purpose of this tutorial is to introduce some of them to you. The strategy mechanism of the PVS theorem prover likewise allows rather powerful capabilities to be built on the basic theorem proving resources of propositional calculus, quantifier reasoning, decision procedures, and rewriting; some of these capabilities are also described here.
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