A tutorial introduction to the PVS proof assistant

Add to your list(s) Download to your calendar using vCal

• Natarajan Shankar (SRI International)
• Friday 30 June 2017, 10:00-11:00
• Seminar Room 2, Newton Institute.

If you have a question about this talk, please contact INI IT.

BPR - Big proof

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 .

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

• All CMS events
• Featured lists
• INI info aggregator
• Isaac Newton Institute Seminar Series
• School of Physical Sciences
• Seminar Room 2, Newton Institute
• bld31

Note that ex-directory lists are not shown.