SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
  SRI Logo

Integration in PVS: Tables, Types, and Model Checking
 by Sam Owre, Dr. John Rushby & Dr. Natarajan Shankar.

Lecture Notes in Computer Science, Number 1217.
From Tools and Algorithms for the Construction and Analysis of Systems TACAS '97.
Edited by Ed Brinksma.
Springer-Verlag, Enschede, The Netherlands.
April, 1997.
Pages 366–383.

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. 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.
BibTEX Entry
    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 = {}


About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2024 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy