Proof Mate: An Interactive Proof Helper for PVSThis paper presents Proof Mate, an interactive proof helper for the PVS verification system. The helper is integrated in VSCode-PVS, the Visual Studio Code extension for PVS. It extends the capabilities of VSCode-PVS by introducing new functionalities for suggesting proof commands, sketching proof attempts, and repairing broken proofs during interactive proof sessions. This work further aligns VSCode-PVS to the functionalities provided by modern development tools, with the ultimate aim to facilitate the adoption of formal methods in engineering practices and education.
Document ID
20220007348
Acquisition Source
Langley Research Center
Document Type
Presentation
Authors
Paolo Masci (National Institute of Aerospace Hampton, Virginia, United States)
Aaron Dutle (Langley Research Center Hampton, Virginia, United States)