Dynamic Synthesis of Program Invariants using Genetic Programming

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

  title =        "Dynamic Synthesis of Program Invariants using Genetic
  author =       "Luigi Cardamone and Andrea Mocci and Carlo Ghezzi",
  pages =        "617--624",
  booktitle =    "Proceedings of the 2011 IEEE Congress on Evolutionary
  year =         "2011",
  editor =       "Alice E. Smith",
  month =        "5-8 " # jun,
  address =      "New Orleans, USA",
  organization = "IEEE Computational Intelligence Society",
  publisher =    "IEEE Press",
  ISBN =         "0-7803-8515-2",
  keywords =     "genetic algorithms, genetic programming, SBSE,
                 invariant formula, logic formulae, loop manipulating
                 array, program comprehension, program in verification,
                 statement execution, symbolic program manipulation,
                 transformation rule, iterative methods, program
                 verification, symbol manipulation",
  DOI =          "doi:10.1109/CEC.2011.5949677",
  abstract =     "In the field of software engineering, invariant
                 detection techniques have been proposed to overcome the
                 problem of software behaviour comprehension. If the
                 code of a program is available, combining symbolic and
                 concrete execution has been shown to provide an
                 effective method to derive logic formulae that describe
                 a program's behavior. However, symbolic execution does
                 not work very well with loops, and thus such methods
                 are not able to derive useful descriptions of programs
                 containing loops. In this paper, we present a
                 preliminary approach that aims to integrate genetic
                 programming to synthesise a logic formula that
                 describes the behaviour of a loop. Such formula could
                 be integrated in a symbolic execution based approach
                 for invariant detection to synthesize a complex program
                 behaviour. We present a specific representation of
                 formulae that works well with loops manipulating
                 arrays. The technique has been validated with a set of
                 relevant examples with increasing complexity. The
                 preliminary results are promising and show the
                 feasibility of our approach.",
  notes =        "CEC2011 sponsored by the IEEE Computational
                 Intelligence Society, and previously sponsored by the
                 EPS and the IET.",

Genetic Programming entries for Luigi Cardamone Andrea Mocci Carlo Ghezzi