![[Search]](/static/images/search.gif){kind=small}
![[A-Z Index]](/static/images/az.gif){kind=small}
![[Contact]](/static/images/contact.gif){kind=small}
![[University of Cambridge]](/static/images/identifier2.gif){kind=small}
![[Talks.cam]](/static/images/talkslogosmall.gif)
Natarajan Shankar (SRI International)
Friday 30 June 2017, 10:00-11:00
A tutorial introduction to the PVS proof assistant
- đ¤ Speaker: Natarajan Shankar (SRI International)
- đ Date & Time: Friday 30 June 2017, 10:00 - 11:00
- đ Venue: Seminar Room 2, Newton Institute
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 .
Series This talk is part of the Isaac Newton Institute Seminar Series series.
Included in Lists
- All CMS events
- bld31
- dh539
- Featured lists
- INI info aggregator
- Isaac Newton Institute Seminar Series
- School of Physical Sciences
- Seminar Room 2, Newton Institute
Note: Ex-directory lists are not shown.