A tutorial introduction to the PVS proof assistant
1 hour 1 min,
878.51 MB,
MPEG-4 Video
640x360,
29.97 fps,
44100 Hz,
1.92 Mbits/sec
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) |
Distribution: | World (downloadable) |
Explicit content: | No |
Aspect Ratio: | 16:9 |
Screencast: | No |
Bumper: | UCS Default |
Trailer: | UCS Default |
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) |