SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
     
  SRI Logo

A Case-Study in Component-Based Mechanical Verification of Fault-Tolerant Programs
 by Dr. John Rushby, Dr. Natarajan Shankar & Sandeep S. Kulkarni.

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 Dykstra's token ring program in a component-based manner. We also demonstrate the advantages of component based mechanical verification.
Files
 













 

About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2017 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy