{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,7]],"date-time":"2024-08-07T11:10:35Z","timestamp":1723029035533},"reference-count":42,"publisher":"MIT Press","issue":"3","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Evolutionary Computation"],"published-print":{"date-parts":[[2018,9]]},"abstract":"<jats:p>Conventional genetic programming (GP) can guarantee only that synthesized programs pass tests given by the provided input-output examples. The alternative to such a test-based approach is synthesizing programs by formal specification, typically realized with exact, nonheuristic algorithms. In this article, 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.<\/jats:p>","DOI":"10.1162\/evco_a_00228","type":"journal-article","created":{"date-parts":[[2018,5,22]],"date-time":"2018-05-22T15:19:27Z","timestamp":1527002367000},"page":"441-469","source":"Crossref","is-referenced-by-count":9,"title":["Counterexample-Driven Genetic Programming: Heuristic Program Synthesis from Formal Specifications"],"prefix":"10.1162","volume":"26","author":[{"given":"Iwo","family":"B\u0142\u0105dek","sequence":"first","affiliation":[{"name":"Institute of Computing Science, Poznan University of Technology, Pozna\u0144, 60-965, Poland"}]},{"given":"Krzysztof","family":"Krawiec","sequence":"additional","affiliation":[{"name":"Institute of Computing Science, Poznan University of Technology, Pozna\u0144, 60-965, Poland"}]},{"given":"Jerry","family":"Swan","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of York, York, YO10 5GH, UK"}]}],"member":"281","reference":[{"key":"B1","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-85729-018-2_2"},{"key":"B2","first-page":"1","author":"Alur R.","year":"2013","journal-title":"Formal Methods in Computer-Aided Design"},{"key":"B3","first-page":"3","author":"Alur R.","year":"2015","journal-title":"Proceedings Fourth Workshop on Synthesis"},{"key":"B4","first-page":"319","author":"Alur R.","year":"2017","journal-title":"Proceedings of Tools and Algorithms for the Construction and Analysis of Systems\u201423rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software Part I"},{"key":"B5","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1145\/1321631.1321693","author":"Arcuri A.","year":"2007","journal-title":"Proceedings of the 22nd IEEE\/ACM International Conference on Automated Software Engineering"},{"key":"B6","first-page":"259:412","author":"Arcuri A.","year":"2014","journal-title":"Information Science"},{"key":"B7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"B10","volume-title":"Test driven development: By example","author":"Beck","year":"2002"},{"key":"B11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-55696-3_1"},{"key":"B12","volume-title":"Formal methods: State of the art and new directions","author":"Boca P. P.","year":"2009","edition":"1"},{"key":"B13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22183-0_20"},{"issue":"3","key":"B14","volume":"1","author":"Cohen B.","year":"1994","journal-title":"Formal Aspects of Computing"},{"key":"B15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"B16","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44811-X_34"},{"key":"B17","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1145\/1836089.1836091","author":"Gulwani S.","year":"2010","journal-title":"Proceedings of the 12th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming"},{"key":"B18","author":"Gulwani S.","year":"2010","journal-title":"Component based synthesis applied to bitvector programs"},{"key":"B19","unstructured":"Harman, M., Jia, Y., and Langdon, W. B. (2014).Babel Pidgin: SBSE can grow and graft entirely new functionality into a real world system(pp. 247\u2013252). Cham: Springer."},{"key":"B20","first-page":"90","author":"Haynes T.","year":"1996","journal-title":"Proceedings of the 1st Annual Conference on Genetic Programming"},{"key":"B21","doi-asserted-by":"publisher","DOI":"10.1007\/s11432-011-4200-4"},{"key":"B22","doi-asserted-by":"publisher","DOI":"10.1109\/TEVC.2014.2362729"},{"key":"B23","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"B24","doi-asserted-by":"publisher","DOI":"10.1145\/1706356.1706364"},{"key":"B25","first-page":"78","author":"Hofmann M.","year":"2008","journal-title":"Proceedings of the 31st Annual German Conference on Advances in Artificial Intelligence"},{"key":"B26","volume-title":"Nonparametric statistical methods","author":"Hollander M.","year":"2013"},{"key":"B27","first-page":"215","author":"Jha S.","year":"2010","journal-title":"29th International Conference on Software Engineering"},{"key":"B28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71605-1_11"},{"key":"B29","doi-asserted-by":"publisher","DOI":"10.4135\/9781849208499"},{"key":"B30","doi-asserted-by":"publisher","DOI":"10.1145\/2103746.2103758"},{"key":"B31","unstructured":"Katz, G., and Peled, D. (2008).Genetic programming and model checking: Synthesizing new mutual exclusion algorithms(pp. 33\u201347). Berlin, Heidelberg: Springer."},{"key":"B32","first-page":"70","author":"Katz G.","year":"2014","journal-title":"Proceedings 15th International Workshop on Verification of Infinite-State Systems"},{"key":"B33","first-page":"1","author":"Katz G.","year":"2016","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"B34","author":"Kocsis Z.","year":"2014","journal-title":"Workshop on Semantic Methods in Genetic Programming, Parallel Problem Solving from Nature, Ljubljana, Slovenia"},{"key":"B35","first-page":"1141","author":"Kocsis Z. A.","year":"2016","journal-title":"Genetic Improvement 2016 Workshop"},{"key":"B36","first-page":"60:157","author":"Kocsis Z. A.","year":"2017","journal-title":"Journal of Automated Reasoning"},{"key":"B37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-27565-9"},{"key":"B38","doi-asserted-by":"publisher","DOI":"10.1145\/3071178.3071224"},{"key":"B39","first-page":"829","author":"Luke S.","year":"2002","journal-title":"Proceedings of the Genetic and Evolutionary Computation Conference (GECCO)"},{"key":"B40","doi-asserted-by":"publisher","DOI":"10.1145\/181668.181671"},{"key":"B41","author":"Raghothaman M.","year":"2014","journal-title":"Computing Research Repository"},{"key":"B42","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-017-0270-2"},{"key":"B43","doi-asserted-by":"publisher","DOI":"10.1145\/1168918.1168907"},{"key":"B44","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706337"}],"container-title":["Evolutionary Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mitpressjournals.org\/doi\/pdf\/10.1162\/evco_a_00228","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,2]],"date-time":"2023-09-02T19:20:37Z","timestamp":1693682437000},"score":1,"resource":{"primary":{"URL":"https:\/\/direct.mit.edu\/evco\/article\/26\/3\/441-469\/1070"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,9]]},"references-count":42,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2018,9]]}},"alternative-id":["10.1162\/evco_a_00228"],"URL":"https:\/\/doi.org\/10.1162\/evco_a_00228","relation":{},"ISSN":["1063-6560","1530-9304"],"issn-type":[{"value":"1063-6560","type":"print"},{"value":"1530-9304","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,9]]}}}