A Case-Study in Component-Based Mechanical Verification of Fault-Tolerant Programs

Sandeep S. Kulkarni, John Rushby, Natarajan Shankar



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.

Paper:

Slides


BibTeX Entry

@Article{krs99,
  author = 	 {S.~S~.Kulkarni and J.~Rushby and N.~Shankar},
  title = 	 {A Case-Study in Component-Based Mechanical Verification of Fault-Tolerant Programs}, 
  journal = 	 {Proceedings of the 19th IEEE International Conference on Distributed Computing Systems Workshop on Self-Stabilization (WSS'99) Austin, Texas, USA},
  year = 	 {1999},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  month = 	 {June},
  pages = 	 {33--40},
  OPTnote = 	 {},
  OPTannote = 	 {}
}
Return to the publication list
Return to the Sandeep's home page