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

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

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)

Cited In (14)

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

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)