Formalizing Theorems with PVS

XIV Summer Workshop in Mathematics MAT/UnB, Brasília
Classes: January, 18 (Tuesday) and January, 20 (Thursday)

General information

We are going to use the proof assistant PVS (versão 7.1) embeeded on the VS-Code software (VSCode-PVS IDE).
The instalation of PVS is not mandatory for the classes, however we encourage the participants install
the system in their machines in order to work on the exercises.

• It is possible to install VSCode-PVS from the VSCode Marketplace.
• We are going to use the NASA PVS libraries (NASALib) in some examples and exercises.
• Natively, PVS runs over Unix or MacOS plataforms (except, for now, in M1 architectures).
  In order to execute PVS over Windows or MacOS (M1 chip), it is necessary to install a virtual machine.

Program and Material

• Class 1 : 08:00 - 10:30 - January 18, 2022
• Class 2 : 15:10 - 17:10 - January 18, 2022
• Class 3 : 10:30 - 12:30 - January 20, 2022

Lecturers

• Mauricio Ayala-Rincón (UnB)
• Thaynara Arielly de Lima (UFG)