A tutorial introduction to the PVS proof assistant
Duration: 1 hour 1 min
Share this media item:
Embed this media item:
Embed this media item:
About this item
| Description: |
Shankar, N
Friday 30th June 2017 - 10:00 to 11:00 |
|---|
| Created: | 2017-07-21 09:23 |
|---|---|
| Collection: | Big proof |
| Publisher: | Isaac Newton Institute |
| Copyright: | Shankar, N |
| Language: | eng (English) |
| 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.
|
|---|---|
Available Formats
| Format | Quality | Bitrate | Size | |||
|---|---|---|---|---|---|---|
| MPEG-4 Video | 640x360 | 1.92 Mbits/sec | 878.51 MB | View | Download | |
| WebM | 640x360 | 538.5 kbits/sec | 240.59 MB | View | Download | |
| iPod Video | 480x270 | 493.65 kbits/sec | 220.55 MB | View | Download | |
| MP3 | 44100 Hz | 251.02 kbits/sec | 112.15 MB | Listen | Download | |
| Auto * | (Allows browser to choose a format it supports) | |||||