- author = "Thomas Welsch and Vitaliy Kurlin",
- title = "Synthesis through Unification Genetic Programming",
- year = "2020",
- editor = "Carlos Artemio {Coello Coello} and Arturo Hernandez Aguirre and Josu Ceberio Uribe and Mario Garza Fabre and Gregorio {Toscano Pulido} and Katya Rodriguez-Vazquez and Elizabeth Wanner and Nadarajen Veerapen and Efren Mezura Montes and Richard Allmendinger and Hugo Terashima Marin and Markus Wagner and Thomas Bartz-Beielstein and Bogdan Filipic and Heike Trautmann and Ke Tang and John Koza and Erik Goodman and William B. Langdon and Miguel Nicolau and Christine Zarges and Vanessa Volz and Tea Tusar and Boris Naujoks and Peter A. N. Bosman and Darrell Whitley and Christine Solnon and Marde Helbig and Stephane Doncieux and Dennis G. Wilson and Francisco {Fernandez de Vega} and Luis Paquete and Francisco Chicano and Bing Xue and Jaume Bacardit and Sanaz Mostaghim and Jonathan Fieldsend and Oliver Schuetze and Dirk Arnold and Gabriela Ochoa and Carlos Segura and Carlos Cotta and Michael Emmerich and Mengjie Zhang and Robin Purshouse and Tapabrata Ray and Justyna Petke and Fuyuki Ishikawa and Johannes Lengler and Frank Neumann",
- isbn13 = "9781450371285",
- publisher = "Association for Computing Machinery",
- publisher_address = "New York, NY, USA",
-
URL = "
https://doi.org/10.1145/3377930.3390208",
-
DOI = "
doi:10.1145/3377930.3390208",
- booktitle = "Proceedings of the 2020 Genetic and Evolutionary Computation Conference",
- pages = "1029--1036",
- size = "8 pages",
- keywords = "genetic algorithms, genetic programming, STUN GP, CDGP, grammatical evolution, divide and conquer, search based program synthesis",
- address = "internet",
- series = "GECCO '20",
- month = jul # " 8-12",
- organisation = "SIGEVO",
-
abstract = "We present a new method, Synthesis through Unification
Genetic Programming (STUN GP), which synthesizes
provably correct programs using a Divide and Conquer
approach. This method first splits the input space by
undergoing a discovery phase that uses
Counterexample-Driven Genetic Programming (CDGP) to
identify a set of programs that are provably correct
under unknown unification constraints. The STUN GP
method then computes these restraints by synthesizing
predicates with CDGP that strictly map inputs to
programs where the output will be correct.
This method builds on previous work towards applying Genetic Programming (GP) to Syntax Guided Synthesis (SyGus) problems that seek to synthesize programs adhering to a formal specification rather than a fixed set of input-output examples. We show that our method is more scalable than previous CDGP variants, solving several benchmarks from the SyGus Competition that cannot be solved by CDGP. STUN GP significantly cuts into the gap between GP and state-of-the-art SyGus solvers and further demonstrates Genetic Programming's potential for Program Synthesis.",
-
notes = "program synthesis, proof tool, SMTlib, microsoft Z3,
generates counter-examples. Grammar. max4( x y x
w)...max12() check-synth. CLIA. STUN GP
Also known as \cite{10.1145/3377930.3390208} GECCO-2020 A Recombination of the 29th International Conference on Genetic Algorithms (ICGA) and the 25th Annual Genetic Programming Conference (GP)",
