6th October, 2025
14:00-15:00 "PVS by Example"
César A. Muñoz (NASA LaRC Formal Methods)
General introduction to PVS and its specification language through an example. Mariano is working on a presentation on the PVS logic and theorem prover, using vscode-pvs.
15:00-16:00 "PVS logic and theorem prover"
Mariano M. Moscato (Analytic Mechanics Associates Inc.)
Presentation on the PVS logic and theorem prover using VSCode-PVS.
16:30-18:30 "Hands-on PVS for mathematicians!"
Thaynara Arielly de Lima (Federal University of Goiás) & Mauricio Ayala-Rincón (University of Brasília)
Interactive proof theorem exercise using as a case study Fürstenberger's topological proof on the infinitude of primes
Exercises: pvs file
Instruction to attendants: Install the PVS VS Code extension on your (OS or Linux PC). This is the easiest way!
Only a limited number of computers will be provided to the attendees during the tutorial. See installation instructions at VSCode-PVS.