Counterexample-Driven Genetic Programming: Stochastic Synthesis of Provably Correct Programs

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

  author =       "Krzysztof Krawiec and Iwo Bladek and Jerry Swan and 
                 John H. Drake",
  title =        "Counterexample-Driven Genetic Programming: Stochastic
                 Synthesis of Provably Correct Programs",
  booktitle =    "Proceedings of the Twenty-Seventh International Joint
                 Conference on Artificial Intelligence (IJCAI-18)",
  year =         "2018",
  editor =       "Jerome Lang",
  pages =        "5304--5308",
  address =      "Stockholm",
  publisher_address = "Vienna University of Technology, Institute of
                 Discrete Mathematics and Geometry, E104 Wiedner
                 Hauptstr. 8-10, A-1040 Vienna, Austria",
  month =        "13-19 " # jul,
  publisher =    "International Joint Conferences on Artificial
  keywords =     "genetic algorithms, genetic programming, Typed Genetic
                 Programming, CDGP, Heuristic Search and Game Playing,
                 Meta-Reasoning and Meta-heuristics, Agent-based and
                 Multi-agent Systems, Formal Verification, Validation
                 and Synthesis",
  isbn13 =       "978-0-9992411-2-7",
  URL =          "",
  URL =          "",
  DOI =          "doi:10.24963/ijcai.2018/742",
  size =         "5 pages",
  abstract =     "Genetic programming is an effective technique for
                 inductive synthesis of programs from tests, i.e.
                 training examples of desired input-output behaviour.
                 Programs synthesized in this way are not guaranteed to
                 generalize beyond the training set, which is
                 unacceptable in many applications. We present
                 Counterexample-Driven Genetic Programming (CDGP) that
                 employs evolutionary search to synthesize provably
                 correct programs from formal specifications. CDGP
                 employs a Satisfiability Modulo Theories (SMT) solver
                 to formally verify programs in the evaluation phase. A
                 failed verification produces counterexamples that are
                 in turn used to calculate fitness and thereby drive the
                 search process. When compared with a range of
                 approaches on a suite of state-of-the-art
                 specification-based synthesis benchmarks, CDGP
                 systematically outperforms them, typically synthesising
                 correct programs faster and using fewer tests.",
  notes =        "Lexicase selection. SAT solver, SMT solvers Microsoft

                 Benchmarks: CountPos, IsSeries, IsSorted, Max, Median,
                 Range, Search, Sum Max tree depth 12.

                 The source code of CDGP, along with specifications of
                 problems, is available at

                 This paper is an abridged version of a paper titled
                 Counterexample-Driven Genetic Programming
                 \cite{Krawiec:2017:GECCOa} that won a best-paper award
                 at the GECCO-2017 conference.",

Genetic Programming entries for Krzysztof Krawiec Iwo Bladek Jerry Swan John H Drake