@inproceedings{tacas2017,
	Author = {ThanhVu Nguyen and Deepak Kapur and Westley Weimer and Stephanie Forrest},
Title = {{Connecting Program Synthesis and Reachability: Automatic Program Repair using Test-Input Generation}},
	Booktitle = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
	Pages = {301-318},
	Publisher = {Springer},
	Url_code = {https://bitbucket.org/nguyenthanhvuh/ceti/},
        Url_paper = {Pub/equiv.pdf},
	Url_slides = {Pub/equiv_pres.pdf},			
	Year = {2017},
	Bibbase_Note = {{Complete proofs appear in the technical report version at https://cse-apps.unl.edu/facdb/publications/TR-UNL-CSE-2016-0005.pdf}},
	Keywords = {Program synthesis; program reachability; reduction proof; equivalence proof; automated program repair; 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.}
}

{"_id":"A5i65gK32d4nCFLfZ","bibbaseid":"nguyen-kapur-weimer-forrest-connectingprogramsynthesisandreachabilityautomaticprogramrepairusingtestinputgeneration-2017","downloads":0,"creationDate":"2017-04-18T04:47:40.432Z","title":"Connecting Program Synthesis and Reachability: Automatic Program Repair using Test-Input Generation","author_short":["Nguyen, T.","Kapur, D.","Weimer, W.","Forrest, S."],"year":2017,"bibtype":"inproceedings","biburl":"http://cse.unl.edu/~tnguyen/vu_bibs1.bib","bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"firstnames":["ThanhVu"],"propositions":[],"lastnames":["Nguyen"],"suffixes":[]},{"firstnames":["Deepak"],"propositions":[],"lastnames":["Kapur"],"suffixes":[]},{"firstnames":["Westley"],"propositions":[],"lastnames":["Weimer"],"suffixes":[]},{"firstnames":["Stephanie"],"propositions":[],"lastnames":["Forrest"],"suffixes":[]}],"title":"Connecting Program Synthesis and Reachability: Automatic Program Repair using Test-Input Generation","booktitle":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","pages":"301-318","publisher":"Springer","url_code":"https://bitbucket.org/nguyenthanhvuh/ceti/","url_paper":"Pub/equiv.pdf","url_slides":"Pub/equiv_pres.pdf","year":"2017","bibbase_note":"Complete proofs appear in the technical report version at https://cse-apps.unl.edu/facdb/publications/TR-UNL-CSE-2016-0005.pdf","keywords":"Program synthesis; program reachability; reduction proof; equivalence proof; automated program repair; 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.","bibtex":"@inproceedings{tacas2017,\n\tAuthor = {ThanhVu Nguyen and Deepak Kapur and Westley Weimer and Stephanie Forrest},\nTitle = {{Connecting Program Synthesis and Reachability: Automatic Program Repair using Test-Input Generation}},\n\tBooktitle = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},\n\tPages = {301-318},\n\tPublisher = {Springer},\n\tUrl_code = {https://bitbucket.org/nguyenthanhvuh/ceti/},\n Url_paper = {Pub/equiv.pdf},\n\tUrl_slides = {Pub/equiv_pres.pdf},\t\t\t\n\tYear = {2017},\n\tBibbase_Note = {{Complete proofs appear in the technical report version at https://cse-apps.unl.edu/facdb/publications/TR-UNL-CSE-2016-0005.pdf}},\n\tKeywords = {Program synthesis; program reachability; reduction proof; equivalence proof; automated program repair; test input generation},\n\tAbstract = {We prove that certain formulations of program synthesis and reachability are equivalent.\nSpecifically, our constructive proof shows the reductions between the\ntemplate-based synthesis problem, which generates a program in a\npre-specified form, and the reachability problem, which decides the reachability of a program location.\nThis establishes a link between the two research fields and allows for the transfer of techniques and results between them.\n\nTo demonstrate the equivalence, we develop a program repair prototype using reachability tools. \nWe 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.\nThose test values correspond to repairs for the original program.\nPreliminary results suggest that our approach compares favorably to other repair methods.}\n}\n\n\t\t\t\t\t\t\t\n","author_short":["Nguyen, T.","Kapur, D.","Weimer, W.","Forrest, S."],"key":"tacas2017","id":"tacas2017","bibbaseid":"nguyen-kapur-weimer-forrest-connectingprogramsynthesisandreachabilityautomaticprogramrepairusingtestinputgeneration-2017","role":"author","urls":{" code":"https://bitbucket.org/nguyenthanhvuh/ceti/"," paper":"http://cse.unl.edu/~tnguyen/Pub/equiv.pdf"," slides":"http://cse.unl.edu/~tnguyen/Pub/equiv_pres.pdf"},"keyword":["Program synthesis; program reachability; reduction proof; equivalence proof; automated program repair; test input generation"],"downloads":0},"search_terms":["connecting","program","synthesis","reachability","automatic","program","repair","using","test","input","generation","nguyen","kapur","weimer","forrest"],"keywords":["program synthesis; program reachability; reduction proof; equivalence proof; automated program repair; test input generation"],"authorIDs":[],"dataSources":["AAQcbSuJRTAKBGbG3"]}