Program Validation and Verification in PVS

Software for the PVS Tutorial

This course is organized as a hands-on experience. Therefore, we strongly encourage installing PVS 7.1 and the VSCode-PVS IDE beforehand. Additionally, we will make use of the NASA PVS libraries (NASALib) 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: PVS runs natively on Unix or MacOS platforms. For the Windows platform, you will need to use VirtualBox.

Installation

Install the VSCode-PVS extension from the Visual Studio Code marketplace, and complete the installation wizard to download of PVS and NASALib.

Download

VirtualBox

Alternatively, you can download a ready-to-use VirtualBox image by hitting the button below.

Download

Program

The tutorial was held virtually on July 11th 2021 under the umbrella of CADE 28 .

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

People

We are a group of formal methods practitioners using PVS for several years on the verification of safety-critical systems. Some of this work was realized under the scope of the NASA Langley Formal Methods Group.

Join us and other PVS enthusiasts on this Google group.

Presenter

Paolo Masci

National Institute of Aerospace

Presenter

Mariano Moscato

National Institute of Aerospace

Presenter

César Muñoz

NASA LaRC (Formerly)

Presenter

Aaron Dutle

NASA LaRC

Presenter

Tanner Slagel

NASA LaRC

Support

Marco Feliú

National Institute of Aerospace