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

Thanh Vu Nguyen; Westley Weimer; Deepak Kapur; Stephanie Forrest

doi:10.1007/978-3-662-54577-5_17

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

Thanh Vu Nguyen, Westley Weimer, Deepak Kapur, Stephanie Forrest

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

11 Scopus citations

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 program. Preliminary results suggest that our approach compares favorably to other repair methods.

Original language	English (US)
Title of host publication	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
Editors	Tiziana Margaria , Axel Legay
Publisher	Springer Verlag
Pages	301-318
Number of pages	18
ISBN (Print)	9783662545768
DOIs	https://doi.org/10.1007/978-3-662-54577-5_17
State	Published - 2017
Externally published	Yes
Event	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 - Uppsala, Sweden Duration: Apr 22 2017 → Apr 29 2017

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	10205 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	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
Country/Territory	Sweden
City	Uppsala
Period	4/22/17 → 4/29/17

Keywords

Automated program repair
Program reachability
Program synthesis
Program verification
Reduction proof
Test-input generation

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-662-54577-5_17

Cite this

Nguyen, T. V., Weimer, W., Kapur, D., & Forrest, S. (2017). Connecting program synthesis and reachability: Automatic program repair using test-input generation. In T. Margaria , & A. Legay (Eds.), 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 (pp. 301-318). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10205 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-662-54577-5_17

Connecting program synthesis and reachability: Automatic program repair using test-input generation. / Nguyen, Thanh Vu; Weimer, Westley; Kapur, Deepak et al.
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. ed. / Tiziana Margaria ; Axel Legay. Springer Verlag, 2017. p. 301-318 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10205 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Nguyen, TV, Weimer, W, Kapur, D & Forrest, S 2017, Connecting program synthesis and reachability: Automatic program repair using test-input generation. in T Margaria & A Legay (eds), 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. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10205 LNCS, Springer Verlag, pp. 301-318, 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, Uppsala, Sweden, 4/22/17. https://doi.org/10.1007/978-3-662-54577-5_17

Nguyen TV, Weimer W, Kapur D, Forrest S. Connecting program synthesis and reachability: Automatic program repair using test-input generation. In Margaria T, Legay A, editors, 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. Springer Verlag. 2017. p. 301-318. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-662-54577-5_17

Nguyen, Thanh Vu ; Weimer, Westley ; Kapur, Deepak et al. / Connecting program synthesis and reachability : Automatic program repair using test-input generation. 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. editor / Tiziana Margaria ; Axel Legay. Springer Verlag, 2017. pp. 301-318 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{d52c46d20fe64f96b796dab76385117b,

title = "Connecting program synthesis and reachability: Automatic program repair using test-input generation",

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 program. Preliminary results suggest that our approach compares favorably to other repair methods.",

keywords = "Automated program repair, Program reachability, Program synthesis, Program verification, Reduction proof, Test-input generation",

author = "Nguyen, {Thanh Vu} and Westley Weimer and Deepak Kapur and Stephanie Forrest",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag GmbH Germany 2017.; 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 ; Conference date: 22-04-2017 Through 29-04-2017",

year = "2017",

doi = "10.1007/978-3-662-54577-5_17",

language = "English (US)",

isbn = "9783662545768",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "301--318",

editor = "{Margaria }, Tiziana and Axel Legay",

booktitle = "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",

}

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 - 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 -

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

Abstract

Publication series

Other

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this