VSCode-PVS

VSCode-PVS is a modern integrated development environment for the Prototype Verification System (PVS). This new environment integrates the editing and proof management functionalities of PVS in Visual Studio Code, a popular code editor widely used by software developers. VSCode-PVS provides functionalities that developers expect to find in modern verification tools, but are not available in the standard Emacs front-end of PVS, such as auto-completion, point-and-click navigation of definitions, live diagnostics for errors, and literate programming.

VSCode-PVS is publicly available under NASA's Open Source Agreement from GitHub.

Publications

• Paolo Masci and Aaron Dutle, Proof Mate: an Interactive Proof Helper for PVS (tool paper), Proceedings of the 14th NASA Formal Methods Symposium (NFM 2022), Lecture Notes in Computer Science, Vol. 13260, pp. 809-815, 2022. BibTeX Reference.
• Paolo Masci and César Muñoz, An Integrated Development Environment for the Prototype Verification System, Electronic Proceedings in Theoretical Computer Science, Vol. 310, pp. 35-49, 2019. BibTeX Reference.

The tag identifies links that are outside the NASA domain