An Integrated Development Environment for the Prototype Verification System

An Integrated Development Environment for the Prototype Verification System

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 p...

Full description

Bibliographic Details
Main Authors: Paolo Masci, César A. Muñoz
Format: Article
Language:English
Published: Open Publishing Association 2019-12-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1912.10632v1
id doaj-a8e0f44e349a43cba5306f25f83dd88b
record_format Article
spelling doaj-a8e0f44e349a43cba5306f25f83dd88b2020-11-25T01:48:33ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802019-12-01310Proc. F-IDE 2019354910.4204/EPTCS.310.5:2An Integrated Development Environment for the Prototype Verification SystemPaolo Masci0César A. Muñoz1 National Institute of Aerospace NASA 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.http://arxiv.org/pdf/1912.10632v1
collection DOAJ
language English
format Article
sources DOAJ
author Paolo Masci
César A. Muñoz
spellingShingle Paolo Masci
César A. Muñoz
An Integrated Development Environment for the Prototype Verification System
Electronic Proceedings in Theoretical Computer Science
author_facet Paolo Masci
César A. Muñoz
author_sort Paolo Masci
title An Integrated Development Environment for the Prototype Verification System
title_short An Integrated Development Environment for the Prototype Verification System
title_full An Integrated Development Environment for the Prototype Verification System
title_fullStr An Integrated Development Environment for the Prototype Verification System
title_full_unstemmed An Integrated Development Environment for the Prototype Verification System
title_sort integrated development environment for the prototype verification system
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2019-12-01
description 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.
url http://arxiv.org/pdf/1912.10632v1
work_keys_str_mv AT paolomasci anintegrateddevelopmentenvironmentfortheprototypeverificationsystem
AT cesaramunoz anintegrateddevelopmentenvironmentfortheprototypeverificationsystem
AT paolomasci integrateddevelopmentenvironmentfortheprototypeverificationsystem
AT cesaramunoz integrateddevelopmentenvironmentfortheprototypeverificationsystem
_version_ 1725011528927674368

Similar Items