In this paper, we concentrate on mechanical verification of synthesis algorithms that add multitolerance to fault-intolerant programs using the theorem prover PVS. Multitolerance is desirable when a program is subject to different classes of faults and for each class, a different level of fault-tolerance has to be guaranteed. With this verification, we formally prove the correctness of the synthesis algorithms, which in turn shows that that any program synthesized by them is indeed \emph{correct-by-construction}. We effectively \emph{reuse} formal proofs of our previous work on a fixpoint theory on finite sets and a fault-tolerance theory developed for the case where programs are subject to a single class of faults. We believe manual reuse of proofs may suggest ways to automate them for verification of similar types of synthesis algorithms.
Paper:
Return to the publication list
Return to the Sandeep's home page