TY - GEN
T1 - Connecting program synthesis and reachability
T2 - 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017
AU - Nguyen, Thanh Vu
AU - Weimer, Westley
AU - Kapur, Deepak
AU - Forrest, Stephanie
N1 - Funding Information:
This research was partially supported by NSF awards CCF 1248069, CNS 1619098, CNS 1619123, as well as AFOSR grant FA8750-11-2-0039 and DARPA grant FA8650-10-C-7089.
Publisher Copyright:
© Springer-Verlag GmbH Germany 2017.
PY - 2017
Y1 - 2017
N2 - 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 program. Preliminary results suggest that our approach compares favorably to other repair methods.
AB - 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 program. Preliminary results suggest that our approach compares favorably to other repair methods.
KW - Automated program repair
KW - Program reachability
KW - Program synthesis
KW - Program verification
KW - Reduction proof
KW - Test-input generation
UR - http://www.scopus.com/inward/record.url?scp=85017497166&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85017497166&partnerID=8YFLogxK
U2 - 10.1007/978-3-662-54577-5_17
DO - 10.1007/978-3-662-54577-5_17
M3 - Conference contribution
AN - SCOPUS:85017497166
SN - 9783662545768
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 301
EP - 318
BT - Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings
A2 - Margaria , Tiziana
A2 - Legay, Axel
PB - Springer Verlag
Y2 - 22 April 2017 through 29 April 2017
ER -