Theorem Proving for Verification
John Rushby
Tutorial presented at
MOVEP'2k: Modelling and Verification of
Parallel Processes, Nantes, France, June 2000.
© Springer-Verlag (LNCS 2067). The final version is available at
the Springer LNCS site
Abstract
The challenges in using theorem proving for verification of parallel
systems are to achieve adequate automation, and to allow human guidance
to be expressed in terms of the system under examination rather than
the mechanisms of the prover. This paper provides an overview of
techniques that address these challenges.
gzipped postscript,
or
plain postscript
or
pdf
or
crude ascii (for your Palm Pilot)
Slides
gzipped postscript,
or
plain postscript
or
pdf
or
crude ascii (for your Palm Pilot)
BibTeX Entry
@INPROCEEDINGS{Rushby00:Movep2k,
AUTHOR = {John Rushby},
TITLE = {Theorem Proving for Verification},
BOOKTITLE = {Modelling and Verification of Parallel Processes: MOVEP 2000},
MONTH = jun,
YEAR = 2000,
EDITOR = {Franck Cassez and Claude Jard and Brigitte Rozoy and Mark Dermot Ryan},
ADDRESS = {Nantes, France},
PAGES = {39--57},
PUBLISHER = {springer Verlag},
SERIES = {Lecture Notes in Computer Science},
NUMBER = 2067,
URL = {http://www.csl.sri.com/~rushby/movep2k.html}
}
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page