Authors

Judy Crow, Sam Owre, John Rushby, N. Shankar, and Dave Stringer-Calvert

CSL Technical Report, March 30, 2001

Abstract

We explore ways to enhance the utility of PVS for evaluating, testing, and animating PVS specifications. The PVS ground evaluator is the focus of the work. We describe a mechanism to provide semantic attachments for PVS symbols while preserving soundness, and discuss strategies to provide a generic framework for integrating independently developed applications with PVS. We explore these capabilities in the current system, but conclude that more effective functionality requires extensions to PVS. Recommendations for these extensions are outlined.

gzipped postscript, or plain postscript or PDF

BibTeX Entry

@techreport{PVS-attachments,
        AUTHOR = {Judy Crow and Sam Owre and John Rushby and N. Shankar and Dave Stringer-Calvert},
        TITLE = {Evaluating, Testing, and Animating {PVS} Specifications},
        MONTH = mar,
        YEAR = 2001,
        INSTITUTION = {Computer Science Laboratory, SRI International},
        ADDRESS = {Menlo Park, CA}
}