Please use this identifier to cite or link to this item:
Title: Library Management for PVS
Authors: Romero, Miguel
Rocha Niño, Hernán Camilo
Keywords: Lenguajes de descripción
Issue Date: 27-Oct-2016
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

Files in This Item:
File Description SizeFormat 
paper.pdf292.06 kBAdobe PDFView/Open

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.