Please use this identifier to cite or link to this item:
|Title:||Library Management for PVS|
Rocha Niño, Hernán Camilo
|Keywords:||Lenguajes de descripción|
|Abstract:||The Prototype Verification System (PVS) is a specification language integrated with support tools and a theorem prover. One mechanism for extending and improving PVS is through the development of libraries, i.e., collections of mechanized theories in the language of PVS. This paper presents the pvslm tool: (i) a description language for annotating PVS libraries, with a small footprint but expressive enough for describing complex dependencies among library theories; and (ii) an implementation for managing PVS libraries annotated with this language, offering support for several library sources. The usefulness of the tool is illustrated in this paper with a detailed step-by-step guide on how to manage the current version of the NASA PVS Library with both pvslm’s annotation language and implementation.|
|Appears in Collections:||IF - Working papers|
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.