Enhancing Automated Program Repair with Deductive Verification

Xuan-Bach Le, Quang Loc Le, David Lo, Claire Le Goues

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    131 Downloads (Pure)


    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 assemantic 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.
    Original languageEnglish
    Title of host publicationICSME 2016
    Subtitle of host publication32nd IEEE International Conference on Software Maintenance and Evolution
    Publication statusPublished - 16 Jan 2017
    Event32nd IEEE International Conference on Software Maintenance and Evolution - Raleigh, United States
    Duration: 2 Oct 20167 Oct 2016
    Conference number: 32


    Conference32nd IEEE International Conference on Software Maintenance and Evolution
    Abbreviated titleICSME 2016
    Country/TerritoryUnited States
    Internet address


    Dive into the research topics of 'Enhancing Automated Program Repair with Deductive Verification'. Together they form a unique fingerprint.

    Cite this