
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 CarlJohan H. Seger. SpringerVerlag, 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
(proofswanted.ps).
BibT_{E}X 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 CarlJohan {H.} Seger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {780},
PAGES = {163173},
ADDRESS = {Vancouver, Canada},
MONTH = {aug},
PUBLISHER = {SpringerVerlag},
URL = {http://www.csl.sri.com/papers/holwkshop93/}
}
Files

