Mechanical Verification of Automatic Synthesis of Fault-Tolerant Programs

DOI10.1007/11506676_3zbMATH Open1134.68348OpenAlexW2160452497MaRDI QIDQ5458792FDOQ5458792

Authors Sandeep S. Kulkarni, Borzoo Bonakdarpour, Ali Ebnenasir

Publication date 24 April 2008

Published in Logic Based Program Synthesis and Transformation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11506676_3

zbMATH Keywords

PVSFault-toleranceProgram transformationTheorem provingProgram synthesisMechanical verificationAddition of fault tolerance

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Symbolic synthesis of masking fault-tolerant distributed programs
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• scientific article; zbMATH DE number 1107558
• A compositional framework for fault tolerance by specification transformation
• Automated constraint-based addition of nonmasking and stabilizing fault-tolerance

Cited in

(14)

• Formal verification of mobile robot protocols
• Facilitating the design of fault tolerance in transaction level SystemC programs
• Automating the addition of fault tolerance with discrete controller synthesis
• A Mechanically Checked Generation of Correlating Programs Directed by Structured Syntactic Differences
• Synthesizing bounded-time 2-phase fault recovery
• A case study in the mechanical verification of fault tolerance
• Weakest invariant generation for automated addition of fault-tolerance
• Automated program repair using formal verification techniques
• Automatic verification of fault-tolerant register emulations
• A compositional framework for fault tolerance by specification transformation
• Model-based construction and verification of critical systems using composition and partial refinement
• Synthesis of fault-tolerant embedded systems using games: from theory to practice
• A mechanical analysis of program verification strategies
• Symbolic synthesis of masking fault-tolerant distributed programs

Describes a project that uses

Uses Software

• HOL/SPIN
• PVS

This page was built for publication: Mechanical Verification of Automatic Synthesis of Fault-Tolerant Programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5458792)