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.

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).

@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/}
}

• holwkshop93.dvi
• holwkshop93.pdf
• holwkshop93.ps
• proofs-wanted.pdf
• proofs-wanted.ps