skip to content
 

A tutorial introduction to the PVS proof assistant

Presented by: 
Natarajan Shankar SRI International
Date: 
Friday 30th June 2017 - 10:00 to 11:00
Venue: 
INI Seminar Room 2
Abstract: 

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,  https://github.com/nasa/pvslib).   The tutorial gives a brief overview of the language, logic, and proof infrastructure of PVS.


The video for this talk should appear here if JavaScript is enabled.
If it doesn't, something may have gone wrong with our embedded player.
We'll get it fixed as soon as possible.
Presentation Material: 
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons