Finding and fixing faults
Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Applications of game theory (91A80)
The promises of fault localization and correction for finite state systems sound like magic. However, the algorithm proposed by the authors makes intuitive sense, and it is given a reasonably clear exposition in the paper. The algorithm extracts a ``correction from a winning strategy for a game, constructed from the original program and its specification (expressed in linear temporal logic). The authors apply their algorithm to six examples: unfortunately, all six examples are small in scope and tersely presented. It remains unclear whether larger examples remain tractable with this level of automation.
- ``More deterministic vs. ``smaller Büchi automata for efficient LTL model checking
- A theory of diagnosis from first principles
- An algorithm for strongly connected component analysis in \(n \log n\) symbolic steps
- Church's Problem Revisited
- Computer Aided Verification
- Computer aided verification. 8th international conference, CAV '96, New Brunswick, NJ, USA, July 31 -- August 3, 1996. Proceedings
- Correct Hardware Design and Verification Methods
- Deterministic generators and games for LTL fragments
- Diagnosing multiple faults
- Enhancing model checking in verification by AI techniques
- Fault Localization and Correction with QBF
- scientific article; zbMATH DE number 1670781 (Why is no real title available?)
- scientific article; zbMATH DE number 4124989 (Why is no real title available?)
- scientific article; zbMATH DE number 1982201 (Why is no real title available?)
- scientific article; zbMATH DE number 1744961 (Why is no real title available?)
- scientific article; zbMATH DE number 2087625 (Why is no real title available?)
- scientific article; zbMATH DE number 2089877 (Why is no real title available?)
- scientific article; zbMATH DE number 918600 (Why is no real title available?)
- scientific article; zbMATH DE number 1392310 (Why is no real title available?)
- scientific article; zbMATH DE number 3189696 (Why is no real title available?)
- Lazy abstraction
- Model-based diagnosis of hardware designs
- Myths about the mutual exclusion problem
- On observability of discrete-event systems
- On the synthesis of strategies in infinite games
- Repair of Boolean Programs with an Application to C
- The directed subgraph homeomorphism problem
- Tools and Algorithms for the Construction and Analysis of Systems
- Tools and Algorithms for the Construction and Analysis of Systems
- Vacuity in synthesis
- Must fault localization for program repair
- CTL update of Kripke models through protections
- Synthesizing non-vacuous systems
- Graph Games and Reactive Synthesis
- Symbolic model checking in non-Boolean domains
- Fault Localization and Correction with QBF
- A game-theoretic approach to fault diagnosis and identification of hybrid systems
- On faults and faulty programs
- Correct Hardware Design and Verification Methods
- Computer Aided Verification
- Repair of Boolean Programs with an Application to C
- Defect and evaluations
- Program repair without regret
- Bug localization by constructing reduced traces
This page was built for publication: Finding and fixing faults
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q414907)
