University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > A tutorial introduction to the PVS proof assistant

A tutorial introduction to the PVS proof assistant

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

If you have a question about this talk, please contact info@newton.ac.uk.

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2017 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity