An Integrated Development Environment for the Prototype Verification System

TL;DR

The paper introduces VSCode-PVS, a modern IDE for the Prototype Verification System that enhances usability with features like auto-completion and live diagnostics, aiming to lower the barrier for industry adoption of formal verification.

Contribution

It presents a new integrated environment for PVS within Visual Studio Code, improving user experience and functionality over the traditional Emacs interface.

Findings

Enhanced user interface with auto-completion and navigation

Live diagnostics improve error detection during development

Better integration with modern development workflows

Abstract

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.