Evaluating, Testing, and Animating PVS Specifications

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

CSL Technical Report, March 30, 2001


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

        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