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

7 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 languageEnglish (US)
Title of host publicationTools 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
EditorsTiziana Margaria , Axel Legay
PublisherSpringer Verlag
Pages301-318
Number of pages18
ISBN (Print)9783662545768
DOIs
StatePublished - 2017
Externally publishedYes
Event23rd 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 2017Apr 29 2017

Publication series

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

Other

Other23rd 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
CountrySweden
City Uppsala
Period4/22/174/29/17

Keywords

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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Connecting program synthesis and reachability: Automatic program repair using test-input generation'. Together they form a unique fingerprint.

Cite this