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

Using PVS to Prove Some Theorems of David Parnas
 by Dr. John Rushby & Mandayam Srivas.

Lecture Notes in Computer Science, Volume 780.
From Higher Order Logic Theorem Proving and its Applications (6th International Workshop, HUG '93.
Edited by Jeffrey J. Joyce and Carl-Johan H. Seger.
Springer-Verlag, Vancouver, Canada.
August, 1993.
Pages 163–173.


Abstract
David Parnas (in a paper in the same proceedings) describes some theorems representative of those encountered in support of certification of software for the Darlington nuclear reactor. We describe the verification of these theorems using PVS. Note : A copy of Parnas's paper is available as a postscript file below (proofs-wanted.ps).
BibTEX Entry
@inproceedings{holwkshop93,
    AUTHOR = {John Rushby and Mandayam Srivas},
    TITLE = {Using {PVS} to Prove Some Theorems of David Parnas},
    BOOKTITLE = {Higher Order Logic Theorem Proving and its Applications (6th International Workshop, {HUG} '93},
    YEAR = {1993},
    EDITOR = {Jeffrey {J.} Joyce and Carl-Johan {H.} Seger},
    SERIES = {Lecture Notes in Computer Science},
    VOLUME = {780},
    PAGES = {163--173},
    ADDRESS = {Vancouver, Canada},
    MONTH = {aug},
    PUBLISHER = {Springer-Verlag},
    URL = {http://www.csl.sri.com/papers/holwkshop93/}
}
Files
 













 

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