NASA logo

+ Contact NASA

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.


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

The tag identifies links that are outside the NASA domain


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.

Paolo Masci

National Institute of Aerospace

Mariano Moscato

National Institute of Aerospace

César Muñoz

NASA Langley Research Center

Aaron Dutle

NASA Langley Research Center

Tanner Slagel

NASA Langley Research Center

Marco Feliú

National Institute of Aerospace