Home Intro Wiki Docs FAQ Download Bugs Mail FM Tools

Integration in PVS: Tables, Types, and Model Checking

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


Authors

Sam Owre, John Rushby and N. Shankar

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 or 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/}
}
Home Intro Wiki Docs FAQ Download Bugs Mail FM Tools

Last modified: Wed 24 Nov 2010 14:12 PST
Maintainer: Sam Owre