Evaluating, Testing, and Animating PVS Specifications
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}
}
Having trouble reading our papers?
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page