{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,17]],"date-time":"2025-10-17T13:55:54Z","timestamp":1760709354051,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":35,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,7,1]],"date-time":"2017-07-01T00:00:00Z","timestamp":1498867200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"National Science Centre, Poland","award":["2014\/15\/B\/ST6\/05205"],"award-info":[{"award-number":["2014\/15\/B\/ST6\/05205"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,7]]},"DOI":"10.1145\/3071178.3071224","type":"proceedings-article","created":{"date-parts":[[2017,6,30]],"date-time":"2017-06-30T17:59:28Z","timestamp":1498845568000},"page":"953-960","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":19,"title":["Counterexample-driven genetic programming"],"prefix":"10.1145","author":[{"given":"Krzysztof","family":"Krawiec","sequence":"first","affiliation":[{"name":"Poznan University of Technology, Poznan, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Iwo","family":"B\u0142\u0105dek","sequence":"additional","affiliation":[{"name":"Poznan University of Technology, Poznan, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jerry","family":"Swan","sequence":"additional","affiliation":[{"name":"University of York"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,7]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Jorge Sousa Pinto, and Sim\u00e3o Melo de Sousa.","author":"Almeida Jos\u00e9 Bacelar","year":"2011","unstructured":"Jos\u00e9 Bacelar Almeida , Maria Jo\u00e3o Frade , Jorge Sousa Pinto, and Sim\u00e3o Melo de Sousa. 2011 . An Overview of Formal Methods Tools and Techniques. Springer London , London, 15--44. Jos\u00e9 Bacelar Almeida, Maria Jo\u00e3o Frade, Jorge Sousa Pinto, and Sim\u00e3o Melo de Sousa. 2011. An Overview of Formal Methods Tools and Techniques. Springer London, London, 15--44."},{"key":"e_1_3_2_1_2_1","volume-title":"Formal Methods in Computer-Aided Design (FMCAD)","author":"Alur Rajeev","year":"2013","unstructured":"Rajeev Alur , Rastislav Bodik , Garvit Juniwal , Milo M. K. Martin , Mukund Raghothaman , Sanjit Seshia , Rajdeep Singh , Armando Solar-Lezama , Emina Torlak , and Abhishek Udupa . 2013. Syntax-guided synthesis . In Formal Methods in Computer-Aided Design (FMCAD) , 2013 . IEEE , 1--8. Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit Seshia, Rajdeep Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. 2013. Syntax-guided synthesis. In Formal Methods in Computer-Aided Design (FMCAD), 2013. IEEE, 1--8."},{"key":"e_1_3_2_1_3_1","volume-title":"Proceedings Fourth Workshop on Synthesis, SYNT 2015","author":"Alur Rajeev","year":"2015","unstructured":"Rajeev Alur , Dana Fisman , Rishabh Singh , and Armando Solar-Lezama . 2015 . Results and Analysis of SyGuS-Comp'15 . In Proceedings Fourth Workshop on Synthesis, SYNT 2015 , San Francisco, CA, USA, 18th July 2015. 3--26. Rajeev Alur, Dana Fisman, Rishabh Singh, and Armando Solar-Lezama. 2015. Results and Analysis of SyGuS-Comp'15. In Proceedings Fourth Workshop on Synthesis, SYNT 2015, San Francisco, CA, USA, 18th July 2015. 3--26."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1321631.1321693"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ins.2009.12.019"},{"key":"e_1_3_2_1_7_1","unstructured":"Clark Barrett Pascal Fontaine and Cesare Tinelli. 2016. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org. (2016).  Clark Barrett Pascal Fontaine and Cesare Tinelli. 2016. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org. (2016)."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Dines Bj\u00f8rner and Cliff B. Jones (Eds.). 1978. The Vienna Development Method: The Meta-Language. Springer-Verlag London UK UK.  Dines Bj\u00f8rner and Cliff B. Jones (Eds.). 1978. The Vienna Development Method: The Meta-Language . Springer-Verlag London UK UK.","DOI":"10.1007\/3-540-08766-4"},{"key":"e_1_3_2_1_9_1","volume-title":"Formal Methods: State of the Art and New Directions","author":"Boca Paul P.","year":"2009","unstructured":"Paul P. Boca , Jonathan P. Bowen , and Jawed I Siddiqi . 2009 . Formal Methods: State of the Art and New Directions ( 1 st ed.). Springer Publishing Company, Inc orporated. Paul P. Boca, Jonathan P. Bowen, and Jawed I Siddiqi. 2009. Formal Methods: State of the Art and New Directions (1st ed.). Springer Publishing Company, Incorporated.","edition":"1"},{"key":"e_1_3_2_1_10_1","volume-title":"SSBSE","author":"Buries Nathan","year":"2015","unstructured":"Nathan Buries , Edward Bowles , Alexander E. I. Brownlee , Zoltan A. Kocsis , Jerry Swan , and Nadarajen Veerapen . 2015. Search-Based Software Engineering: 7th International Symposium , SSBSE 2015 , Bergamo, Italy, September 5--7, 2015, Proceedings. Springer International Publishing , Cham, Chapter Object-Oriented Genetic Improvement for Improved Energy Consumption in Google Guava, 255--261. Nathan Buries, Edward Bowles, Alexander E. I. Brownlee, Zoltan A. Kocsis, Jerry Swan, and Nadarajen Veerapen. 2015. Search-Based Software Engineering: 7th International Symposium, SSBSE 2015, Bergamo, Italy, September 5--7, 2015, Proceedings. Springer International Publishing, Cham, Chapter Object-Oriented Genetic Improvement for Improved Energy Consumption in Google Guava, 255--261."},{"volume-title":"Evolutionary Program Sketching","author":"B\u0142\u0105dek Iwo","key":"e_1_3_2_1_11_1","unstructured":"Iwo B\u0142\u0105dek and Krzysztof Krawiec . 2017. Evolutionary Program Sketching . Springer International Publishing , Cham , 3--18. Iwo B\u0142\u0105dek and Krzysztof Krawiec. 2017. Evolutionary Program Sketching. Springer International Publishing, Cham, 3--18."},{"key":"e_1_3_2_1_12_1","volume-title":"PSSE 2004","author":"Cavalcanti A.","year":"2004","unstructured":"A. Cavalcanti , A. Sampaio , and J. Woodcock . 2006. Refinement Techniques in Software Engineering: First Pernambuco Summer School on Software Engineering , PSSE 2004 , Recife, Brazil, November 23- December 5, 2004 , Revised Lectures. Springer Berlin Heidelberg, https:\/\/books.google.co.in\/books?id=aa1qCQAAQBAJ A. Cavalcanti, A. Sampaio, and J. Woodcock. 2006. Refinement Techniques in Software Engineering: First Pernambuco Summer School on Software Engineering, PSSE 2004, Recife, Brazil, November 23-December 5, 2004, Revised Lectures. Springer Berlin Heidelberg, https:\/\/books.google.co.in\/books?id=aa1qCQAAQBAJ"},{"key":"e_1_3_2_1_13_1","volume-title":"A Brief History of Formal Methods. Formal Aspects of Computing 1, 3","author":"Cohen B","year":"1994","unstructured":"B Cohen . 1994. A Brief History of Formal Methods. Formal Aspects of Computing 1, 3 ( 1994 ). B Cohen. 1994. A Brief History of Formal Methods. Formal Aspects of Computing 1, 3 (1994)."},{"volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"de Moura Leonardo","key":"e_1_3_2_1_14_1","unstructured":"Leonardo de Moura and Nikolaj Bj\u00f8rner . 2008. Z3: An Efficient SMT Solver . In Tools and Algorithms for the Construction and Analysis of Systems , C. Ramakrishnan and Jakob Rehof (Eds.). Lecture Notes in Computer Science, Vol. 4963 . Springer Berlin \/ Heidelberg , Berlin, Heidelberg, Chapter 24, 337--340. Leonardo de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, C. Ramakrishnan and Jakob Rehof (Eds.). Lecture Notes in Computer Science, Vol. 4963. Springer Berlin \/ Heidelberg, Berlin, Heidelberg, Chapter 24, 337--340."},{"key":"e_1_3_2_1_16_1","volume-title":"Horning","author":"Guttag John V.","year":"1993","unstructured":"John V. Guttag and James J . Horning . 1993 . Larch : Languages and Tools for Formal Specification. Springer-Verlag New York , Inc., New York, NY, USA. John V. Guttag and James J. Horning. 1993. Larch: Languages and Tools for Formal Specification. Springer-Verlag New York, Inc., New York, NY, USA."},{"key":"e_1_3_2_1_17_1","volume-title":"Langdon","author":"Harman Mark","year":"2014","unstructured":"Mark Harman , Yue Jia , and William B . Langdon . 2014 . Babel Pidgin : SBSE Can Grow and Graft Entirely New Functionality into a Real World System. Springer International Publishing , Cham, 247--252. Mark Harman, Yue Jia, and William B. Langdon. 2014. Babel Pidgin: SBSE Can Grow and Graft Entirely New Functionality into a Real World System. Springer International Publishing, Cham, 247--252."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/TEVC.2014.2362729"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706356.1706364"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85845-4_10"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806833"},{"key":"e_1_3_2_1_23_1","unstructured":"Colin Johnson. 2007. Genetic Programming with Fitness based on Model Checking. In Proceedings of the 10th European Conference on Genetic Programming (Lecture Notes in Computer Science) Marc Ebner Michael O'Neill Anik\u00f3 Ek\u00e1rt Leonardo Vanneschi and Anna Isabel Esparcia-Alc\u00e1zar (Eds.) Vol. 4445. Springer Valencia Spain 114--124. DOI:http:\/\/dx.doi.org\/   Colin Johnson. 2007. Genetic Programming with Fitness based on Model Checking. In Proceedings of the 10th European Conference on Genetic Programming (Lecture Notes in Computer Science) Marc Ebner Michael O'Neill Anik\u00f3 Ek\u00e1rt Leonardo Vanneschi and Anna Isabel Esparcia-Alc\u00e1zar (Eds.) Vol. 4445. Springer Valencia Spain 114--124. DOI:http:\/\/dx.doi.org\/"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103746.2103758"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-88387-6_5"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"crossref","unstructured":"Gal Katz and Doron Peled. 2010. MCGP: A Software Synthesis Tool Based on Model Checking and Genetic Programming. In 8th International Symposium on Automated Technology for Verification and Analysis ATVA 2010 (Lecture Notes in Computer Science) Ahmed Bouajjani and Wei-Ngan Chin (Eds.) Vol. 6252. Springer Singapore 359--364. DOI:http:\/\/dx.doi.org\/   Gal Katz and Doron Peled. 2010. MCGP: A Software Synthesis Tool Based on Model Checking and Genetic Programming. In 8th International Symposium on Automated Technology for Verification and Analysis ATVA 2010 (Lecture Notes in Computer Science) Ahmed Bouajjani and Wei-Ngan Chin (Eds.) Vol. 6252. Springer Singapore 359--364. DOI:http:\/\/dx.doi.org\/","DOI":"10.1007\/978-3-642-15643-4_28"},{"key":"e_1_3_2_1_27_1","volume-title":"International Journal on Software Tools for Technology Transfer","author":"Katz Gal","year":"2016","unstructured":"Gal Katz and Doron Peled . 2016. Synthesizing , correcting and improving code, using model checking-based genetic programming . International Journal on Software Tools for Technology Transfer ( 2016 ), 1--16. Gal Katz and Doron Peled. 2016. Synthesizing, correcting and improving code, using model checking-based genetic programming. International Journal on Software Tools for Technology Transfer (2016), 1--16."},{"key":"e_1_3_2_1_28_1","volume-title":"Asymptotic Genetic Improvement Programming with Type Functors and Catamorphisms. In Workshop on Semantic Methods in Genetic Programming, Parallel Problem Solving from Nature","author":"Kocsis Zoltan","year":"2014","unstructured":"Zoltan Kocsis and Jerry Swan . 2014 . Asymptotic Genetic Improvement Programming with Type Functors and Catamorphisms. In Workshop on Semantic Methods in Genetic Programming, Parallel Problem Solving from Nature , Ljubljana, Slovenia. Zoltan Kocsis and Jerry Swan. 2014. Asymptotic Genetic Improvement Programming with Type Functors and Catamorphisms. In Workshop on Semantic Methods in Genetic Programming, Parallel Problem Solving from Nature, Ljubljana, Slovenia."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908961.2931692"},{"key":"e_1_3_2_1_30_1","unstructured":"Zoltan A. Kocsis and Jerry Swan. 2017 (to appear). Genetic Programming + Proof Search = Automatic Improvement. Journal of Automated Reasoning (2017 (to appear)).  Zoltan A. Kocsis and Jerry Swan. 2017 (to appear). Genetic Programming + Proof Search = Automatic Improvement. Journal of Automated Reasoning (2017 (to appear))."},{"volume-title":"Behavioral Program Synthesis with Genetic Programming. Studies in Computational Intelligence","author":"Krawiec Krzysztof","key":"e_1_3_2_1_31_1","unstructured":"Krzysztof Krawiec . 2015. Behavioral Program Synthesis with Genetic Programming. Studies in Computational Intelligence , Vol. 618 . Springer International Publishing . DOI:http:\/\/dx.doi.org\/ Krzysztof Krawiec. 2015. Behavioral Program Synthesis with Genetic Programming. Studies in Computational Intelligence, Vol. 618. Springer International Publishing. DOI:http:\/\/dx.doi.org\/"},{"key":"e_1_3_2_1_32_1","volume-title":"Test-Driven Development: An Empirical Evaluation of Agile Practice","author":"Madeyski Lech","unstructured":"Lech Madeyski . 2010. Test-Driven Development: An Empirical Evaluation of Agile Practice ( 1 st ed.). Springer Publishing Company, Inc orporated. Lech Madeyski. 2010. Test-Driven Development: An Empirical Evaluation of Agile Practice (1st ed.). Springer Publishing Company, Incorporated.","edition":"1"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/181668.181671"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168917.1168907"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706337"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1968.1972"},{"volume-title":"Using Z: Specification, Refinement, and Proof","author":"Woodcock Jim","key":"e_1_3_2_1_38_1","unstructured":"Jim Woodcock and Jim Davies . 1996. Using Z: Specification, Refinement, and Proof . Prentice-Hall, Inc. , Upper Saddle River, NJ, USA. Jim Woodcock and Jim Davies. 1996. Using Z: Specification, Refinement, and Proof. Prentice-Hall, Inc., Upper Saddle River, NJ, USA."}],"event":{"name":"GECCO '17: Genetic and Evolutionary Computation Conference","sponsor":["SIGEVO ACM Special Interest Group on Genetic and Evolutionary Computation"],"location":"Berlin Germany","acronym":"GECCO '17"},"container-title":["Proceedings of the Genetic and Evolutionary Computation Conference"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3071178.3071224","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3071178.3071224","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:24:05Z","timestamp":1750220645000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3071178.3071224"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,7]]},"references-count":35,"alternative-id":["10.1145\/3071178.3071224","10.1145\/3071178"],"URL":"https:\/\/doi.org\/10.1145\/3071178.3071224","relation":{},"subject":[],"published":{"date-parts":[[2017,7]]},"assertion":[{"value":"2017-07-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}