Enhancing Automated Program Repair with Deductive Verification

Created by W.Langdon from gp-bibliography.bib Revision:1.4549

  author =       "Xuan-Bach D. Le and Quang Loc Le and David Lo and 
                 Claire {Le Goues}",
  booktitle =    "2016 IEEE International Conference on Software
                 Maintenance and Evolution (ICSME)",
  title =        "Enhancing Automated Program Repair with Deductive
  year =         "2016",
  pages =        "428--432",
  month =        "2-10 " # oct,
  address =      "Raleigh, North Carolina, USA",
  keywords =     "genetic algorithms, genetic programming, SBSE,
                 Automated Repair, Deductive Verification, Sound
  URL =          "https://goo.gl/9TS9wo",
  DOI =          "doi:10.1109/ICSME.2016.66",
  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 use 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.",
  notes =        "ICSME 2016

                 Also known as \cite{7816488}",

Genetic Programming entries for Xuan-Bach Dinh Le Quang Loc Le David Lo Claire Le Goues