Program Validation and Verification in PVS
This tutorial was held virtually on July 11th 2021 under the umbrella of CADE 28 .
Software Requirements
This course is organized as a hands-on experience. Therefore, we strongly encourage installing PVS 7.1 and the VSCode-PVS IDE beforehand. Additionally, NASALib, a collection of PVS libraries developed by NASA, is used for some of the examples and exercises. Below you can find different options to install the required software. If you need any assistance, please feel free to reach out to the organizers. Note that PVS runs natively on Unix and MacOS. For the Windows platform, you will need to use VirtualBox.
Option 1: Install the VSCode-PVS extension from the Visual Studio Code marketplace, and complete the installation wizard to download of PVS and NASALib.
Option 2: Alternatively, you can download a ready-to-use VirtualBox image pre-loaded with everything you need for the course.
Program
| 8:00 - 8:05 | Welcome | |
| 8:05 - 8:30 | VSCode-PVS Walkthrough | slides - examples |
| 8:30 - 9:15 | PVS by Example | slides - examples |
| 9:15 - 10:00 | Propositional and Predicate Logic | slides - exercises - solutions |
| 10:00 - 10:30 | Break | |
| 10:30 - 11:30 | Real Number Proving | slides - exercises - solutions |
| 11:30 - 12:00 | Abstract Data Types (1/2) | slides - exercises - solutions |
| 12:00 - 12:30 | Break | |
| 12:30 - 1:00 | Abstract Data Types (2/2) | exercises - solutions |
| 1:00 - 2:00 | Induction, Recursion, and Iteration | slides - exercises - solutions |
| 2:00 - 2:30 | Break | |
| 2:30 - 3:30 | Animation of Functional Specification | slides |
| 3:30 - 4:00 | PVS Teaser | |
| Times in Eastern US Time Zone | download all | |
