S3: Syntax- and semantic-guided repair synthesis via programming by examples

A notable class of techniques for automatic program repair is known as semantics-based. Such techniques, e.g., Angelix, infer semantic specifications via symbolic execution, and then use program synthesis to construct new code that satisfies those inferred specifications. However, the obtained speci...

Full description

Saved in:
Bibliographic Details
Main Authors: LE, Xuan-Bach D., CHU, Duc-Hiep, LO, David, LE GOUES, Claire, VISSER, Willem
Format: text
Language:English
Published: Institutional Knowledge at Singapore Management University 2017
Subjects:
Online Access:https://ink.library.smu.edu.sg/sis_research/3917
https://ink.library.smu.edu.sg/context/sis_research/article/4919/viewcontent/s3.pdf
Tags: Add Tag
No Tags, Be the first to tag this record!
Institution: Singapore Management University
Language: English
id sg-smu-ink.sis_research-4919
record_format dspace
spelling sg-smu-ink.sis_research-49192020-06-09T03:27:10Z S3: Syntax- and semantic-guided repair synthesis via programming by examples LE, Xuan-Bach D. CHU, Duc-Hiep LO, David LE GOUES, Claire VISSER, Willem A notable class of techniques for automatic program repair is known as semantics-based. Such techniques, e.g., Angelix, infer semantic specifications via symbolic execution, and then use program synthesis to construct new code that satisfies those inferred specifications. However, the obtained specifications are naturally incomplete, leaving the synthesis engine with a difficult task of synthesizing a general solution from a sparse space of many possible solutions that are consistent with the provided specifications but that do not necessarily generalize. We present S3, a new repair synthesis engine that leverages programming-by-examples methodology to synthesize high-quality bug repairs. The novelty in S3 that allows it to tackle the sparse search space to create more general repairs is three-fold: (1) A systematic way to customize and constrain the syntactic search space via a domain-specific language, (2) An efficient enumeration- based search strategy over the constrained search space, and (3) A number of ranking features based on measures of the syntactic and semantic distances between candidate solutions and the original buggy program. We compare S3’s repair effectiveness with state-of-the-art synthesis engines Angelix, Enumerative, and CVC4. S3 can successfully and correctly fix at least three times more bugs than the best baseline on datasets of 52 bugs in small programs, and 100 bugs in real-world large programs. 2017-09-01T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/3917 info:doi/10.1145/3106237.3106309 https://ink.library.smu.edu.sg/context/sis_research/article/4919/viewcontent/s3.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University Inductive synthesis Program repair Programming by examples Symbolic execution Software Engineering
institution Singapore Management University
building SMU Libraries
continent Asia
country Singapore
Singapore
content_provider SMU Libraries
collection InK@SMU
language English
topic Inductive synthesis
Program repair
Programming by examples
Symbolic execution
Software Engineering
spellingShingle Inductive synthesis
Program repair
Programming by examples
Symbolic execution
Software Engineering
LE, Xuan-Bach D.
CHU, Duc-Hiep
LO, David
LE GOUES, Claire
VISSER, Willem
S3: Syntax- and semantic-guided repair synthesis via programming by examples
description A notable class of techniques for automatic program repair is known as semantics-based. Such techniques, e.g., Angelix, infer semantic specifications via symbolic execution, and then use program synthesis to construct new code that satisfies those inferred specifications. However, the obtained specifications are naturally incomplete, leaving the synthesis engine with a difficult task of synthesizing a general solution from a sparse space of many possible solutions that are consistent with the provided specifications but that do not necessarily generalize. We present S3, a new repair synthesis engine that leverages programming-by-examples methodology to synthesize high-quality bug repairs. The novelty in S3 that allows it to tackle the sparse search space to create more general repairs is three-fold: (1) A systematic way to customize and constrain the syntactic search space via a domain-specific language, (2) An efficient enumeration- based search strategy over the constrained search space, and (3) A number of ranking features based on measures of the syntactic and semantic distances between candidate solutions and the original buggy program. We compare S3’s repair effectiveness with state-of-the-art synthesis engines Angelix, Enumerative, and CVC4. S3 can successfully and correctly fix at least three times more bugs than the best baseline on datasets of 52 bugs in small programs, and 100 bugs in real-world large programs.
format text
author LE, Xuan-Bach D.
CHU, Duc-Hiep
LO, David
LE GOUES, Claire
VISSER, Willem
author_facet LE, Xuan-Bach D.
CHU, Duc-Hiep
LO, David
LE GOUES, Claire
VISSER, Willem
author_sort LE, Xuan-Bach D.
title S3: Syntax- and semantic-guided repair synthesis via programming by examples
title_short S3: Syntax- and semantic-guided repair synthesis via programming by examples
title_full S3: Syntax- and semantic-guided repair synthesis via programming by examples
title_fullStr S3: Syntax- and semantic-guided repair synthesis via programming by examples
title_full_unstemmed S3: Syntax- and semantic-guided repair synthesis via programming by examples
title_sort s3: syntax- and semantic-guided repair synthesis via programming by examples
publisher Institutional Knowledge at Singapore Management University
publishDate 2017
url https://ink.library.smu.edu.sg/sis_research/3917
https://ink.library.smu.edu.sg/context/sis_research/article/4919/viewcontent/s3.pdf
_version_ 1770573935269642240