2015/03/15 by Heinz Riener, Rüdiger Ehlers, Görschwin Fey
Computer Science · Mathematics · #Abstraction #Algorithm #Computer science #Control flow #Counterexample #Debugging #Discrete mathematics #Mathematics #Model checking #Path (computing) #Program analysis #Programming language #Software #Software Engineering Research #Software Reliability and Analysis Research #Software Testing and Debugging Techniques #Symbolic execution #Theoretical computer science #cs.PL #cs.SE
paper · pdf · doi:10.4204/eptcs.178.3
published in Electronic Proceedings in Theoretical Computer Science 178, 22-32 (Open Publishing Association) · In Proceedings FESCA 2015, arXiv:1503.04378
openalex publication_date 2015/03/15 · arxiv created 2015/03/17 · arxiv updated 2015/03/18 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/05
We propose a path-based approach to program repair for imperative programs. Our repair framework takes as input a faulty program, a logic specification that is refuted, and a hint where the fault may be located. An iterative abstraction refinement loop is then used to repair the program: in each iteration, the faulty program part is re-synthesized considering a symbolic counterexample, where the control-flow is kept concrete but the data-flow is symbolic. The appeal of the idea is two-fold: 1) the approach lazily considers candidate repairs and 2) the repairs are directly derived from the logic specification. In contrast to prior work, our approach is complete for programs with finitely many control-flow paths, i.e., the program is repaired if and only if it can be repaired at the specified fault location. Initial results for small programs indicate that the approach is useful for debugging programs in practice.