Please use this identifier to cite or link to this item:
Exportar a Bibtex Exportar a RIS Exportar a Excel Buscar en google Schoolar Buscar en microsoft academic
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 PDFThumbnail
Show full item record

Page view(s)

checked on Nov 9, 2017

Google ScholarTM


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