Publication Type
Conference Proceeding Article
Version
publishedVersion
Publication Date
10-2016
Abstract
Automated program repair (APR) is a challenging process of detecting bugs, localizing buggy code, generating fix candidates and validating the fixes. Effectiveness of program repair methods relies on the generated fix candidates, and the methods used to traverse the space of generated candidates to search for the best ones. Existing approaches generate fix candidates based on either syntactic searches over source code or semantic analysis of specification, e.g., test cases. In this paper, we propose to combine both syntactic and semantic fix candidates to enhance the search space of APR, and provide a function to effectively traverse the search space. We present an automated repair method based on structured specifications, deductive verification and genetic programming. Given a function with its specification, we utilize a modular verifier to detect bugs and localize both program statements and sub-formulas in the specification that relate to those bugs. While the former are identified as buggy code, the latter are transformed as semantic fix candidates. We additionally generate syntactic fix candidates via various mutation operators. Best candidates, which receives fewer warnings via a static verification, are selected for evolution though genetic programming until we find one satisfying the specification. Another interesting feature of our proposed approach is that we efficiently ensure the soundness of repaired code through modular (or compositional) verification. We implemented our proposal and tested it on C programs taken from the SIR benchmark that are seeded with bugs, achieving promising results.
Keywords
Sound Repair, Automated Repair, Genetic Programming, Deductive Verification, Computer bugs, Semantics, Genetic programming, Syntactics, Benchmark testing, Prototypes
Discipline
Software Engineering
Research Areas
Software and Cyber-Physical Systems
Publication
2016 IEEE International Conference on Software Maintenance and Evolution: ICSME 2016: 2-10 October 2016, Raleigh: Proceedings
ISBN
9781509038060
Identifier
10.1109/ICSME.2016.66
Publisher
IEEE
City or Country
Piscataway, NJ
Citation
LE, Xuan-Bach D.; LE, Quang Loc; LO, David; and GOUES, Claire Le.
Enhancing automated program repair with deductive verification. (2016). 2016 IEEE International Conference on Software Maintenance and Evolution: ICSME 2016: 2-10 October 2016, Raleigh: Proceedings.
Available at: https://ink.library.smu.edu.sg/sis_research/3753
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Additional URL
http://doi.org/10.1109/ICSME.2016.66