Mechanical Verification of Automatic Synthesis of Fault-Tolerant Programs

DOI10.1007/11506676_3MaRDI QIDQ5458792zbMATH OpenOpenAlexFDO

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

Addition of fault toleranceFault-toleranceMechanical verificationProgram synthesisProgram transformationPVSTheorem proving

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

(15)

• Automating the addition of fault tolerance with discrete controller synthesis
• A compositional framework for fault tolerance by specification transformation
• Symbolic synthesis of masking fault-tolerant distributed programs
• Formal verification of mobile robot protocols
• Automatic verification of fault-tolerant register emulations
• Synthesis of fault-tolerant embedded systems using games: from theory to practice
• A Mechanically Checked Generation of Correlating Programs Directed by Structured Syntactic Differences
• Facilitating the design of fault tolerance in transaction level SystemC programs
• scientific article; zbMATH DE number 1107558 (Why is no real title available?)
• 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
• Model-based construction and verification of critical systems using composition and partial refinement
• Synthesizing bounded-time 2-phase fault recovery
• A mechanical analysis of program verification strategies

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)