Synthesizing, Correcting and Improving Code, Using Model Checking-Based Genetic Programming

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

  author =       "Gal Katz and Doron Peled",
  title =        "Synthesizing, Correcting and Improving Code, Using
                 Model Checking-Based Genetic Programming",
  booktitle =    "Proceedings of the 9th International Haifa
                 Verification Conference (HVC 2013)",
  year =         "2013",
  editor =       "Valeria Bertacco and Axel Legay",
  volume =       "8244",
  series =       "Lecture Notes in Computer Science",
  pages =        "246--261",
  address =      "Haifa, Israel",
  month =        nov # " 5-7",
  publisher =    "Springer",
  note =         "Keynote Presentation",
  keywords =     "genetic algorithms, genetic programming, SBSE, STGP",
  bibdate =      "2013-11-21",
  bibsource =    "DBLP,
  isbn13 =       "978-3-319-03076-0",
  URL =          "",
  URL =          "",
  DOI =          "doi:10.1007/978-3-319-03077-7_17",
  size =         "16 pages",
  abstract =     "The use of genetic programming, in combination of
                 model checking and testing, provides a powerful way to
                 synthesise programs. Whereas classical algorithmic
                 synthesis provides alarming high complexity and
                 undecidability results, the genetic approach provides a
                 surprisingly successful heuristics. We describe several
                 versions of a method for synthesising sequential and
                 concurrent systems. To cope with the constraints of
                 model checking and of theorem proving, we combine such
                 exhaustive verification methods with testing. We show
                 several examples where we used our approach to
                 synthesise, improve and correct code.",
  notes =        "Fitness = enhanced model checking. mu plus lambda ES,
                 crossover not implemented. Strongly typed tree GP.
                 Linear Temporal Logic. Streett Automata. Mutual
                 exclusion. Parametric Programs, check is not

                 bug fixing: election of leader protocol
                 architecture=test case. competitive Co-evolution of
                 test cases verses evolving corrected code p257 'reverse
                 the genetic programming direction' p259 'correct an
                 actual error' MCGP tool

                 Hardware and Software: Verification and Testing.

                 See also Synthesis of
                 Parametric Programs using Genetic Programming and Model
                 Checking \cite{DBLP:journals/corr/KatzP14}",

Genetic Programming entries for Gal Katz Doron A Peled