Counterexample-Driven Genetic Programming: Heuristic Program Synthesis from Formal Specifications

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

@Article{Bladek:EC,

• author = "Iwo Bladek and Krzysztof Krawiec and Jerry Swan",
• title = "Counterexample-Driven Genetic Programming: Heuristic Program Synthesis from Formal Specifications",
• journal = "Evolutionary Computation",
• year = "2018",
• volume = "26",
• number = "3",
• pages = "441--469",
• month = "Fall",
• keywords = "genetic algorithms, genetic programming, formal verification, counterexamples, SMT",
• ISSN = "1063-6560",
• DOI = "10.1162/evco_a_00228",
• size = "27 pages",
• abstract = "Conventional genetic programming (GP) can only guarantee that synthesized programs pass tests given by the provided input-output examples. The alternative to such test-based approach is synthesizing programs by formal specification, typically realized with exact, non-heuristic algorithms. In this paper, we build on our earlier study on Counterexample-Based Genetic Programming (CDGP), an evolutionary heuristic that synthesizes programs from formal specifications. The candidate programs in CDGP undergo formal verification with a Satisfiability Modulo Theory (SMT) solver, which results in counterexamples that are subsequently turned into tests and used to calculate fitness. The original CDGP is extended here with a fitness threshold parameter that decides which programs should be verified, a more rigorous mechanism for turning counterexamples into tests, and other conceptual and technical improvements. We apply it to 24 benchmarks representing two domains: the linear integer arithmetic (LIA) and the string manipulation (SLIA) problems, showing that CDGP can reliably synthesize provably correct programs in both domains. We also confront it with two state-of-the art exact program synthesis methods and demonstrate that CDGP effectively trades longer synthesis time for smaller program size.",
• notes = "Extended Paper Invited from GECCO 2017",

}

Genetic Programming entries for Iwo Bladek Krzysztof Krawiec Jerry Swan

Citations