Connecting program synthesis and reachability: automatic program repair using test-input generation

DOI10.1007/978-3-662-54577-5_17MaRDI QIDQ3303900zbMATH OpenOpenAlexFDO

Authors Thanhvu H. Nguyen, Westley Weimer, Deepak Kapur, Stephanie Forrest

Publication date 5 August 2020

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1903.11765

zbMATH Keywords

automated program repairprogram reachabilityprogram synthesisprogram verificationreduction prooftest-input generation

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Abstract: We prove that certain formulations of program synthesis and reachability are equivalent. Specifically, our constructive proof shows the reductions between the template-based synthesis problem, which generates a program in a pre-specified form, and the reachability problem, which decides the reachability of a program location. This establishes a link between the two research fields and allows for the transfer of techniques and results between them. To demonstrate the equivalence, we develop a program repair prototype using reachability tools. We transform a buggy program and its required specification into a specific program containing a location reachable only when the original program can be repaired, and then apply an off-the-shelf test-input generation tool on the transformed program to find test values to reach the desired location. Those test values correspond to repairs for the original programm. Preliminary results suggest that our approach compares favorably to other repair methods.

Recommendations

• Program synthesis with equivalence reduction
• Automatic program repair using formal verification and expression templates
• Counterexample guided inductive synthesis modulo theories
• scientific article; zbMATH DE number 1926611
• Automated repair of heap-manipulating programs using deductive synthesis

Cites work

• Automating string processing in spreadsheets using input-output examples
• Classes of Recursively Enumerable Sets and Their Decision Problems
• Computer Aided Verification
• From program verification to program synthesis
• scientific article; zbMATH DE number 2087570 (Why is no real title available?)
• Specification-based program repair using SAT

Cited in

(4)

• Automated repair of heap-manipulating programs using deductive synthesis
• Program synthesis with equivalence reduction
• Automatic program repair using formal verification and expression templates
• Automated program repair using formal verification techniques

Describes a project that uses

Uses Software

• KLOVER
• Prophet
• SemFix
• Angelix
• CUTE
• BLAST
• DART
• SLAM
• KLEE
• JPF-SE
• CIL
• jCUTE

This page was built for publication: Connecting program synthesis and reachability: automatic program repair using test-input generation

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