From Tools and Algorithms for the Construction and Analysis of Systems TACAS '97. Enschede, The Netherlands. April, 1997.

Authors

Abstract

We have argued previously that the effectiveness of a verification system derives not only from the power of its individual features for expression and deduction, but from the extent to which these capabilities are integrated: the whole is more than the sum of its parts [ZUM95, FTRTFT96]. Here, we illustrate this thesis by describing a simple construct for tabular specifications that was recently added to PVS. Because this construct integrates with other capabilities of PVS, such as typechecker-generated proof obligations, dependent typing, higher-order functions, model checking, and general theorem proving, it can be used for a surprising variety of purposes. We demonstrate this with examples drawn from hardware division algorithms and requirements specifications.

gzipped postscript

postscript

pdf

BibTeX Entry

@inproceedings{pvs-tables:tacas97,
    AUTHOR = {Sam Owre and John Rushby and {N.} Shankar},
    TITLE = {Integration in {PVS:} Tables, Types, and Model Checking},
    BOOKTITLE = {Tools and Algorithms for the Construction and Analysis of Systems {TACAS} '97},
    YEAR = {1997},
    EDITOR = {Ed Brinksma},
    SERIES = {Lecture Notes in Computer Science},
    NUMBER = {1217},
    PAGES = {366-383},
    ADDRESS = {Enschede, The Netherlands},
    MONTH = {apr},
    PUBLISHER = {Springer-Verlag},
    URL = {http://www.csl.sri.com/papers/tacas97/}
}