Presented at Applied Formal Methods - FM-Trends 98, Boppard, Germany, October 1998.

Authors

Abstract

PVS is a comprehensive interactive tool for specification and verification combining an expressive specification language with an integrated suite of tools for theorem proving and model checking. PVS has many academic and industrial users and has been applied to a wide range of verification tasks. In this note, we summarize some of its applications.

gzipped postscript

postscript

BibTeX Entry

@inproceedings{Owre-etal98:FM-TRENDS,
    AUTHOR = {Sam Owre and John Rushby and {N.} Shankar and David Stringer-Calvert},
    TITLE = {{PVS:} An Experience Report},
    BOOKTITLE = {Applied Formal Methods---FM-Trends 98},
    YEAR = {1998},
    EDITOR = {Dieter Hutter and Werner Stephan and Paolo Traverso and Markus Ullman},
    SERIES = {Lecture Notes in Computer Science},
    VOLUME = {1641},
    PAGES = {338--345},
    ADDRESS = {Boppard, Germany},
    MONTH = {oct},
    PUBLISHER = {Springer-Verlag},
    URL = {http://www.csl.sri.com/papers/fmtrends98/}
}