A Case Study in Component-based Mechanical Verification
of Fault-Tolerant Programs
Sandeep Kulkarni, John Rushby, and N. Shankar
ICDCS Workshop on Self-Stabilizing Systems
Abstract
In this paper, we present a case study to demonstrate that the
decomposition of a fault-tolerant program into its components is
useful in its mechanical verification. More specifically, we discuss
our experience in using the theorem prover PVS to verify Dijkstra s
token ring program in a component-based manner. We also demonstrate
the advantages of component based mechanical verification.
PDF
BibTeX Entry
@INPROCEEDINGS{Kulkarni99:SSS,
AUTHOR = {Sandeep Kulkarni and John Rushby and N. Shankar},
TITLE = {A Case Study in Component-based Mechanical Verification
of Fault-Tolerant Programs},
BOOKTITLE = {{ICDCS} Workshop on Self-Stabilizing Systems},
MONTH = jun,
YEAR = 1999,
ADDRESS = {Austin, TX},
ORGANIZATION = {IEEE Computer Society},
PAGES = {33--40}
}
Having trouble reading our papers?
Return to John Rushby's bibliography page
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page