NFM 2025
PVS Day 2025
1st International Workshop on the Prototype Verification System
Collocated with NFM 2025
College of William & Mary, Computer Science Department
Williamsburg, Virginia, USA
June 10th, 2025
Join us for an exciting and collaborative workshop dedicated to the Prototype Verification System! This event aims to bring together users, practitioners, and enthusiasts from around the world to foster a vibrant and supportive community centered around PVS.
- Expert Talks
- Gain insights from leading researchers and practitioners who will share their latest work and innovations involving PVS.
- Community Building
- Network with fellow PVS users, share experiences, and collaborate on projects to advance the use of PVS in various domains.
- Panel Discussions
- Participate in thought-provoking discussions on the future of theorem proving, challenges, and opportunities within the PVS community.
- Showcase of Applications
- Discover diverse applications of PVS across different industries and research areas through presentations and demonstrations.
Whether you are a seasoned PVS user or new to the theorem prover, this workshop offers a unique opportunity to learn, connect, and contribute to the PVS community. Don't miss out on this chance to be part of a global network of like-minded individuals passionate about advancing formal verification and theorem proving.
Tentative Program
All times are in ET.
| 9:00 am | 1h | PVS 8.0 (Main features, PVS2C, etc.) |
| 10:00 am | 30' | VSCode-PVS demo |
| 10:30 am | 15' | ☕️ Break |
| 10:45 am | 45' | Rapid Prototyping & Evaluation with PVSio |
| 11:30 am | 30' | PVS Community (NASALib, collaboration & interaction) |
| 12:00 am | 1h | 🍽️ Lunch |
| 1:00 pm | 1h | Plaidypvs |
| 2:00 pm | 45' | PVS Internals & Debugging Tools for PVS |
| 2:45 pm | 15' | ☕️ Break |
| 3:00 pm | 1h | The Algebra Library and Applications of Quaternions |
| 4:00 pm | 45' | Differential testing with PVSio |
| 4:45 pm | 15' | Closing remarks + Operational Meeting |
Location and Cost
The PVS Day will also be hosted by the Computer Science Department at William & Mary, in Williamsburg, Virginia. Following the NFM spirit, participation in the PVS Day is free, but registration is mandatory (via the NFM registration form).
Organization
- Mariano Moscato (AMA Inc.)
- César Muñoz (NASA)
Contact Us
If you have any question or comment, please reach out via this form.
