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