---
_id: '941'
abstract:
- lang: eng
text: 'Recently there has been a proliferation of automated program repair (APR)
techniques, targeting various programming languages. Such techniques can be generally
classified into two families: syntactic- and semantics-based. Semantics-based
APR, on which we focus, typically uses symbolic execution to infer semantic constraints
and then program synthesis to construct repairs conforming to them. While syntactic-based
APR techniques have been shown successful on bugs in real-world programs written
in both C and Java, semantics-based APR techniques mostly target C programs. This
leaves empirical comparisons of the APR families not fully explored, and developers
without a Java-based semantics APR technique. We present JFix, a semantics-based
APR framework that targets Java, and an associated Eclipse plugin. JFix is implemented
atop Symbolic PathFinder, a well-known symbolic execution engine for Java programs.
It extends one particular APR technique (Angelix), and is designed to be sufficiently
generic to support a variety of such techniques. We demonstrate that semantics-based
APR can indeed efficiently and effectively repair a variety of classes of bugs
in large real-world Java programs. This supports our claim that the framework
can both support developers seeking semantics-based repair of bugs in Java programs,
as well as enable larger scale empirical studies comparing syntactic- and semantics-based
APR targeting Java. The demonstration of our tool is available via the project
website at: https://xuanbachle.github.io/semanticsrepair/ '
author:
- first_name: Xuan
full_name: Le, Xuan
last_name: Le
- first_name: Duc Hiep
full_name: Chu, Duc Hiep
id: 3598E630-F248-11E8-B48F-1D18A9856A87
last_name: Chu
- first_name: David
full_name: Lo, David
last_name: Lo
- first_name: Claire
full_name: Le Goues, Claire
last_name: Le Goues
- first_name: Willem
full_name: Visser, Willem
last_name: Visser
citation:
ama: 'Le X, Chu DH, Lo D, Le Goues C, Visser W. JFIX: Semantics-based repair of
Java programs via symbolic PathFinder. In: Proceedings of the 26th ACM SIGSOFT
International Symposium on Software Testing and Analysis. ACM; 2017:376-379.
doi:10.1145/3092703.3098225'
apa: 'Le, X., Chu, D. H., Lo, D., Le Goues, C., & Visser, W. (2017). JFIX: Semantics-based
repair of Java programs via symbolic PathFinder. In Proceedings of the 26th
ACM SIGSOFT International Symposium on Software Testing and Analysis (pp.
376–379). Santa Barbara, CA, United States: ACM. https://doi.org/10.1145/3092703.3098225'
chicago: 'Le, Xuan, Duc Hiep Chu, David Lo, Claire Le Goues, and Willem Visser.
“JFIX: Semantics-Based Repair of Java Programs via Symbolic PathFinder.” In Proceedings
of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis,
376–79. ACM, 2017. https://doi.org/10.1145/3092703.3098225.'
ieee: 'X. Le, D. H. Chu, D. Lo, C. Le Goues, and W. Visser, “JFIX: Semantics-based
repair of Java programs via symbolic PathFinder,” in Proceedings of the 26th
ACM SIGSOFT International Symposium on Software Testing and Analysis, Santa
Barbara, CA, United States, 2017, pp. 376–379.'
ista: 'Le X, Chu DH, Lo D, Le Goues C, Visser W. 2017. JFIX: Semantics-based repair
of Java programs via symbolic PathFinder. Proceedings of the 26th ACM SIGSOFT
International Symposium on Software Testing and Analysis. ISSTA: International
Symposium on Software Testing and Analysis, 376–379.'
mla: 'Le, Xuan, et al. “JFIX: Semantics-Based Repair of Java Programs via Symbolic
PathFinder.” Proceedings of the 26th ACM SIGSOFT International Symposium on
Software Testing and Analysis, ACM, 2017, pp. 376–79, doi:10.1145/3092703.3098225.'
short: X. Le, D.H. Chu, D. Lo, C. Le Goues, W. Visser, in:, Proceedings of the 26th
ACM SIGSOFT International Symposium on Software Testing and Analysis, ACM, 2017,
pp. 376–379.
conference:
end_date: 2017-07-14
location: Santa Barbara, CA, United States
name: 'ISSTA: International Symposium on Software Testing and Analysis'
start_date: 2017-07-10
date_created: 2018-12-11T11:49:19Z
date_published: 2017-07-10T00:00:00Z
date_updated: 2021-01-12T08:22:05Z
day: '10'
department:
- _id: ToHe
doi: 10.1145/3092703.3098225
language:
- iso: eng
month: '07'
oa_version: None
page: '376 - 379 '
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: Proceedings of the 26th ACM SIGSOFT International Symposium on Software
Testing and Analysis
publication_status: published
publisher: ACM
publist_id: '6478'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'JFIX: Semantics-based repair of Java programs via symbolic PathFinder'
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
year: '2017'
...
---
_id: '942'
abstract:
- lang: eng
text: '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. '
article_processing_charge: No
author:
- first_name: Xuan
full_name: Le, Xuan
last_name: Le
- first_name: Duc Hiep
full_name: Chu, Duc Hiep
id: 3598E630-F248-11E8-B48F-1D18A9856A87
last_name: Chu
- first_name: David
full_name: Lo, David
last_name: Lo
- first_name: Claire
full_name: Le Goues, Claire
last_name: Le Goues
- first_name: Willem
full_name: Visser, Willem
last_name: Visser
citation:
ama: 'Le X, Chu DH, Lo D, Le Goues C, Visser W. S3: Syntax- and semantic-guided
repair synthesis via programming by examples. In: Vol F130154. ACM; 2017:593-604.
doi:10.1145/3106237.3106309'
apa: 'Le, X., Chu, D. H., Lo, D., Le Goues, C., & Visser, W. (2017). S3: Syntax-
and semantic-guided repair synthesis via programming by examples (Vol. F130154,
pp. 593–604). Presented at the FSE: Foundations of Software Engineering, Paderborn,
Germany: ACM. https://doi.org/10.1145/3106237.3106309'
chicago: 'Le, Xuan, Duc Hiep Chu, David Lo, Claire Le Goues, and Willem Visser.
“S3: Syntax- and Semantic-Guided Repair Synthesis via Programming by Examples,”
F130154:593–604. ACM, 2017. https://doi.org/10.1145/3106237.3106309.'
ieee: 'X. Le, D. H. Chu, D. Lo, C. Le Goues, and W. Visser, “S3: Syntax- and semantic-guided
repair synthesis via programming by examples,” presented at the FSE: Foundations
of Software Engineering, Paderborn, Germany, 2017, vol. F130154, pp. 593–604.'
ista: 'Le X, Chu DH, Lo D, Le Goues C, Visser W. 2017. S3: Syntax- and semantic-guided
repair synthesis via programming by examples. FSE: Foundations of Software Engineering
vol. F130154, 593–604.'
mla: 'Le, Xuan, et al. S3: Syntax- and Semantic-Guided Repair Synthesis via Programming
by Examples. Vol. F130154, ACM, 2017, pp. 593–604, doi:10.1145/3106237.3106309.'
short: X. Le, D.H. Chu, D. Lo, C. Le Goues, W. Visser, in:, ACM, 2017, pp. 593–604.
conference:
end_date: 2017-09-08
location: Paderborn, Germany
name: 'FSE: Foundations of Software Engineering'
start_date: 2017-09-04
date_created: 2018-12-11T11:49:19Z
date_published: 2017-09-01T00:00:00Z
date_updated: 2023-09-26T15:38:36Z
day: '01'
department:
- _id: ToHe
doi: 10.1145/3106237.3106309
external_id:
isi:
- '000414279300055'
isi: 1
language:
- iso: eng
month: '09'
oa_version: None
page: 593 - 604
project:
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication_identifier:
isbn:
- 978-145035105-8
publication_status: published
publisher: ACM
publist_id: '6477'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'S3: Syntax- and semantic-guided repair synthesis via programming by examples'
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: F130154
year: '2017'
...
---
_id: '962'
abstract:
- lang: eng
text: 'We present a new algorithm for model counting of a class of string constraints.
In addition to the classic operation of concatenation, our class includes some
recursively defined operations such as Kleene closure, and replacement of substrings.
Additionally, our class also includes length constraints on the string expressions,
which means, by requiring reasoning about numbers, that we face a multi-sorted
logic. In the end, our string constraints are motivated by their use in programming
for web applications. Our algorithm comprises two novel features: the ability
to use a technique of (1) partial derivatives for constraints that are already
in a solved form, i.e. a form where its (string) satisfiability is clearly displayed,
and (2) non-progression, where cyclic reasoning in the reduction process may be
terminated (thus allowing for the algorithm to look elsewhere). Finally, we experimentally
compare our model counter with two recent works on model counting of similar constraints,
SMC [18] and ABC [5], to demonstrate its superior performance.'
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Minh
full_name: Trinh, Minh
last_name: Trinh
- first_name: Duc Hiep
full_name: Chu, Duc Hiep
id: 3598E630-F248-11E8-B48F-1D18A9856A87
last_name: Chu
- first_name: Joxan
full_name: Jaffar, Joxan
last_name: Jaffar
citation:
ama: 'Trinh M, Chu DH, Jaffar J. Model counting for recursively-defined strings.
In: Majumdar R, Kunčak V, eds. Vol 10427. Springer; 2017:399-418. doi:10.1007/978-3-319-63390-9_21'
apa: 'Trinh, M., Chu, D. H., & Jaffar, J. (2017). Model counting for recursively-defined
strings. In R. Majumdar & V. Kunčak (Eds.) (Vol. 10427, pp. 399–418). Presented
at the CAV: Computer Aided Verification, Heidelberg, Germany: Springer. https://doi.org/10.1007/978-3-319-63390-9_21'
chicago: Trinh, Minh, Duc Hiep Chu, and Joxan Jaffar. “Model Counting for Recursively-Defined
Strings.” edited by Rupak Majumdar and Viktor Kunčak, 10427:399–418. Springer,
2017. https://doi.org/10.1007/978-3-319-63390-9_21.
ieee: 'M. Trinh, D. H. Chu, and J. Jaffar, “Model counting for recursively-defined
strings,” presented at the CAV: Computer Aided Verification, Heidelberg, Germany,
2017, vol. 10427, pp. 399–418.'
ista: 'Trinh M, Chu DH, Jaffar J. 2017. Model counting for recursively-defined strings.
CAV: Computer Aided Verification, LNCS, vol. 10427, 399–418.'
mla: Trinh, Minh, et al. Model Counting for Recursively-Defined Strings.
Edited by Rupak Majumdar and Viktor Kunčak, vol. 10427, Springer, 2017, pp. 399–418,
doi:10.1007/978-3-319-63390-9_21.
short: M. Trinh, D.H. Chu, J. Jaffar, in:, R. Majumdar, V. Kunčak (Eds.), Springer,
2017, pp. 399–418.
conference:
end_date: 2017-07-28
location: Heidelberg, Germany
name: 'CAV: Computer Aided Verification'
start_date: 2017-07-24
date_created: 2018-12-11T11:49:26Z
date_published: 2017-01-01T00:00:00Z
date_updated: 2023-09-22T09:58:02Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-319-63390-9_21
editor:
- first_name: Rupak
full_name: Majumdar, Rupak
last_name: Majumdar
- first_name: Viktor
full_name: Kunčak, Viktor
last_name: Kunčak
external_id:
isi:
- '000431900900021'
intvolume: ' 10427'
isi: 1
language:
- iso: eng
month: '01'
oa_version: None
page: 399 - 418
project:
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication_identifier:
issn:
- '03029743'
publication_status: published
publisher: Springer
publist_id: '6443'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Model counting for recursively-defined strings
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 10427
year: '2017'
...