Enhancing automated program repair with deductive verification
Conference Proceeding Article
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.
Sound Repair, Automated Repair, Genetic Programming, Deductive Verification, Computer bugs, Semantics, Genetic programming, Syntactics, Benchmark testing, Prototypes
Software and Cyber-Physical Systems
2016 IEEE International Conference on Software Maintenance and Evolution: ICSME 2016: 2-10 October 2016, Raleigh: Proceedings
City or Country
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. Research Collection School Of Information Systems.
Available at: http://ink.library.smu.edu.sg/sis_research/3753
This document is currently not available here.