- author = "Krzysztof Krawiec and Iwo Bladek and Jerry Swan",
- title = "Counterexample-driven Genetic Programming",
- booktitle = "Proceedings of the Genetic and Evolutionary Computation Conference",
- series = "GECCO '17",
- year = "2017",
- address = "Berlin, Germany",
- pages = "953--960",
- acmid = "3071224",
- publisher = "ACM",
- publisher_address = "New York, NY, USA",
- month = "15-19 " # jul,
- note = "Best paper",
- keywords = "genetic algorithms, genetic programming, SAT, SMT, counterexample, formal verification, program synthesis",
- isbn13 = "978-1-4503-4920-8",
-
URL = "
http://doi.acm.org/10.1145/3071178.3071224",
-
DOI = "
doi:10.1145/3071178.3071224",
- size = "8 pages",
- abstract = "Genetic programming is an effective technique for inductive synthesis of programs from training examples of desired input-output behaviour (tests). 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 so drive the search process. When compared against a range of approaches on a suite of state-of-the-art specification-based synthesis benchmarks, CDGP systematically outperforms them, typically synthesizing correct programs faster and using fewer tests.",
-
notes = "Also known as
\cite{Krawiec:2017:CGP:3071178.3071224}
See also \cite{Krawiec:2018:IJCA}
GECCO-2017 A Recombination of the 26th International Conference on Genetic Algorithms (ICGA-2017) and the 22nd Annual Genetic Programming Conference (GP-2017)",
