An Integrated Development Environment for the Prototype Verification System
This addresses the steep learning curve problem for software developers using formal verification tools, but it is incremental as it builds on existing PVS technology.
The paper tackles the barrier to adopting formal verification tools in industry by presenting VSCode-PVS, a modern integrated development environment for the Prototype Verification System (PVS), which integrates editing and proof management into Visual Studio Code with features like auto-completion and live diagnostics.
The steep learning curve of formal technologies is a well-known barrier to the adoption of formal verification tools in industry. This paper presents VSCode-PVS, 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. The main features and architecture of the environment are presented, along with a comparison with other similar tools.