skip to content

A tutorial introduction to the PVS proof assistant

Presented by: 
Natarajan Shankar
Friday 30th June 2017 - 10:00 to 11:00
INI Seminar Room 2
The Prototype Verification System (PVS) is an interactive proof assistant developed at SRI International.  The PVS specification language extends higher-order logic with predicate subtypes, dependent types, inductive datatypes, and parametric theories.  These features make typechecking undecidable, or more accurately, decidable modulo proof obligations.  The interactive proof assistant includes automated support for contextual  simplification, rewriting, and SAT/SMT solving. PVS has been used to formalize large libraries (see, for example,   The tutorial gives a brief overview of the language, logic, and proof infrastructure of PVS.
Presentation Material: 
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons