{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T10:27:56Z","timestamp":1790936876784,"version":"4.1.0"},"publisher-location":"New York, NY, USA","reference-count":48,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,10,26]],"date-time":"2018-10-26T00:00:00Z","timestamp":1540512000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"National Research Foundation","award":["NRF2014NCR-NCR001-21"],"award-info":[{"award-number":["NRF2014NCR-NCR001-21"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,10,26]]},"DOI":"10.1145\/3236024.3236049","type":"proceedings-article","created":{"date-parts":[[2018,10,29]],"date-time":"2018-10-29T12:06:00Z","timestamp":1540814760000},"page":"389-399","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":31,"title":["Symbolic execution with existential second-order constraints"],"prefix":"10.1145","author":[{"given":"Sergey","family":"Mechtaev","sequence":"first","affiliation":[{"name":"National University of Singapore, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alberto","family":"Griggio","sequence":"additional","affiliation":[{"name":"Fondazione Bruno Kessler, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alessandro","family":"Cimatti","sequence":"additional","affiliation":[{"name":"Fondazione Bruno Kessler, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Abhik","family":"Roychoudhury","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2018,10,26]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Ignasi Ab\u00edo Robert Nieuwenhuis Albert Oliveras and Enric Rodr\u00edguez-Carbonell. 2013.  Ignasi Ab\u00edo Robert Nieuwenhuis Albert Oliveras and Enric Rodr\u00edguez-Carbonell. 2013."},{"key":"e_1_3_2_1_2_1","unstructured":"A parametric approach for smaller and better encodings of cardinality constraints. In CP. Springer 80\u201396.  A parametric approach for smaller and better encodings of cardinality constraints. In CP. Springer 80\u201396."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837628"},{"key":"e_1_3_2_1_4_1","volume-title":"Mukund Raghothaman, Sanjit A Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa.","author":"Alur Rajeev","year":"2013","unstructured":"Rajeev Alur , Rastislav Bodik , Garvit Juniwal , Milo MK Martin , Mukund Raghothaman, Sanjit A Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. 2013 . Syntax-guided synthesis. In FMCAD. IEEE. Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo MK Martin, Mukund Raghothaman, Sanjit A Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. 2013. Syntax-guided synthesis. In FMCAD. IEEE."},{"key":"e_1_3_2_1_5_1","volume-title":"Scaling Enumerative Program Synthesis via Divide and Conquer","author":"Alur Rajeev","unstructured":"Rajeev Alur , Arjun Radhakrishna , and Abhishek Udupa . 2017. Scaling Enumerative Program Synthesis via Divide and Conquer . In TACAS. Springer , 319\u2013336. Rajeev Alur, Arjun Radhakrishna, and Abhishek Udupa. 2017. Scaling Enumerative Program Synthesis via Divide and Conquer. In TACAS. Springer, 319\u2013336."},{"key":"e_1_3_2_1_6_1","unstructured":"Clark W Barrett Roberto Sebastiani Sanjit A Seshia Cesare Tinelli etal 2009.  Clark W Barrett Roberto Sebastiani Sanjit A Seshia Cesare Tinelli et al. 2009."},{"key":"e_1_3_2_1_7_1","volume-title":"Handbook of satisfiability 185","author":"Satisfiability","year":"2009","unstructured":"Satisfiability modulo theories. Handbook of satisfiability 185 ( 2009 ), 825\u2013885. Satisfiability modulo theories. Handbook of satisfiability 185 (2009), 825\u2013885."},{"key":"e_1_3_2_1_8_1","unstructured":"Osbert Bastani Saswat Anand and Alex Aiken. 2015.  Osbert Bastani Saswat Anand and Alex Aiken. 2015."},{"key":"e_1_3_2_1_9_1","unstructured":"Specification inference using context-free language reachability. In POPL. ACM 553\u2013566.  Specification inference using context-free language reachability. In POPL. ACM 553\u2013566."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106255"},{"key":"e_1_3_2_1_11_1","first-page":"209","article-title":"KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs","volume":"8","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar , Daniel Dunbar , Dawson R Engler , 2008 . KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs .. In OSDI , Vol. 8. 209 \u2013 224 . Cristian Cadar, Daniel Dunbar, Dawson R Engler, et al. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs.. In OSDI, Vol. 8. 209\u2013224.","journal-title":"OSDI"},{"key":"e_1_3_2_1_12_1","volume-title":"Bastiaan Joost Schaafsma, and Roberto Sebastiani","author":"Cimatti Alessandro","year":"2013","unstructured":"Alessandro Cimatti , Alberto Griggio , Bastiaan Joost Schaafsma, and Roberto Sebastiani . 2013 . Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, and Roberto Sebastiani. 2013."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1323293.1294274"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1098\/rsta.2015.0403"},{"key":"e_1_3_2_1_16_1","unstructured":"Leonardo De Moura and Nikolaj Bj\u00f8rner. 2008.  Leonardo De Moura and Nikolaj Bj\u00f8rner. 2008."},{"key":"e_1_3_2_1_17_1","volume-title":"An efficient SMT solver. TACAS","year":"2008","unstructured":"Z3 : An efficient SMT solver. TACAS ( 2008 ), 337\u2013340. Z3: An efficient SMT solver. TACAS (2008), 337\u2013340."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993529"},{"key":"e_1_3_2_1_19_1","unstructured":"Joxan Jaffar Vijayaraghavan Murali Jorge Navas and Andrew Santosa. 2012.  Joxan Jaffar Vijayaraghavan Murali Jorge Navas and Andrew Santosa. 2012."},{"key":"e_1_3_2_1_20_1","volume-title":"A symbolic execution tool for verification","author":"TRACER","unstructured":"TRACER : A symbolic execution tool for verification . In CAV. Springer , 758\u2013766. TRACER: A symbolic execution tool for verification. In CAV. Springer, 758\u2013766."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806833"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/581339.581397"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2610384.2610388"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594334"},{"key":"e_1_3_2_1_26_1","volume-title":"A systematic study of automated program repair: Fixing 55 out of 105 bugs for $8 each","author":"Goues Claire Le","unstructured":"Claire Le Goues , Michael Dewey-Vogt , Stephanie Forrest , and Westley Weimer . 2012. A systematic study of automated program repair: Fixing 55 out of 105 bugs for $8 each . In ICSE. IEEE , 3\u201313. Claire Le Goues, Michael Dewey-Vogt, Stephanie Forrest, and Westley Weimer. 2012. A systematic study of automated program repair: Fixing 55 out of 105 bugs for $8 each. In ICSE. IEEE, 3\u201313."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786811"},{"key":"e_1_3_2_1_28_1","unstructured":"Fan Long and Martin Rinard. 2016.  Fan Long and Martin Rinard. 2016."},{"key":"e_1_3_2_1_29_1","volume-title":"298\u2013312","author":"Automatic","year":"2016","unstructured":"Automatic patch generation by learning correct code. POPL 51, 1 ( 2016 ), 298\u2013312 . Automatic patch generation by learning correct code. POPL 51, 1 (2016), 298\u2013312."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180247"},{"key":"e_1_3_2_1_31_1","volume-title":"Shin Hwei Tan, and Abhik Roychoudhury","author":"Mechtaev Sergey","year":"2018","unstructured":"Sergey Mechtaev , Gao Xiang , Shin Hwei Tan, and Abhik Roychoudhury . 2018 . Sergey Mechtaev, Gao Xiang, Shin Hwei Tan, and Abhik Roychoudhury. 2018."},{"key":"e_1_3_2_1_32_1","unstructured":"Test-equivalence Analysis for Automatic Patch Generation. TOSEM (2018).  Test-equivalence Analysis for Automatic Patch Generation. TOSEM (2018)."},{"key":"e_1_3_2_1_33_1","volume-title":"Directfix: Looking for simple program repairs","author":"Mechtaev Sergey","year":"2015","unstructured":"Sergey Mechtaev , Jooyong Yi , and Abhik Roychoudhury . 2015 . Directfix: Looking for simple program repairs . In ICSE. IEEE Press , 448\u2013458. Sergey Mechtaev, Jooyong Yi, and Abhik Roychoudhury. 2015. Directfix: Looking for simple program repairs. In ICSE. IEEE Press, 448\u2013458."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884807"},{"key":"e_1_3_2_1_35_1","unstructured":"Elliott Mendelson. 2009.  Elliott Mendelson. 2009."},{"key":"e_1_3_2_1_36_1","unstructured":"Introduction to mathematical logic. CRC press.  Introduction to mathematical logic. CRC press."},{"key":"e_1_3_2_1_37_1","unstructured":"Hoang Duong Thien Nguyen Dawei Qi Abhik Roychoudhury and Satish Chandra. 2013.  Hoang Duong Thien Nguyen Dawei Qi Abhik Roychoudhury and Satish Chandra. 2013."},{"key":"e_1_3_2_1_38_1","volume-title":"Program repair via semantic analysis","author":"Semfix","unstructured":"Semfix : Program repair via semantic analysis . In ICSE. IEEE Press , 772\u2013781. Semfix: Program repair via semantic analysis. In ICSE. IEEE Press, 772\u2013781."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884845"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2211616.2211622"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/WCRE.2012.51"},{"key":"e_1_3_2_1_42_1","volume-title":"Counterexample-guided quantifier instantiation for synthesis in SMT","author":"Reynolds Andrew","unstructured":"Andrew Reynolds , Morgan Deters , Viktor Kuncak , Cesare Tinelli , and Clark Barrett . 2015. Counterexample-guided quantifier instantiation for synthesis in SMT . In CAV. Springer , 198\u2013216. Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, and Clark Barrett. 2015. Counterexample-guided quantifier instantiation for synthesis in SMT. In CAV. Springer, 198\u2013216."},{"key":"e_1_3_2_1_43_1","unstructured":"Jo\u00e3o P Marques Silva and Karem A Sakallah. 1997.  Jo\u00e3o P Marques Silva and Karem A Sakallah. 1997."},{"key":"e_1_3_2_1_44_1","unstructured":"GRASP\u00e2\u0102\u0164a new search algorithm for satisfiability. In CAV. IEEE Computer Society 220\u2013227.  GRASP\u00e2\u0102\u0164a new search algorithm for satisfiability. In CAV. IEEE Computer Society 220\u2013227."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786825"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950295"},{"key":"e_1_3_2_1_47_1","volume-title":"Pex\u2013white box test generation for .Net. Tests and Proofs","author":"Tillmann Nikolai","year":"2008","unstructured":"Nikolai Tillmann and Jonathan De Halleux . 2008. Pex\u2013white box test generation for .Net. Tests and Proofs ( 2008 ), 134\u2013153. Nikolai Tillmann and Jonathan De Halleux. 2008. Pex\u2013white box test generation for .Net. Tests and Proofs (2008), 134\u2013153."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3092703.3092714"}],"event":{"name":"ESEC\/FSE '18: 26th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering","location":"Lake Buena Vista FL USA","acronym":"ESEC\/FSE '18","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3236024.3236049","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3236024.3236049","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:57:26Z","timestamp":1750208246000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3236024.3236049"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10,26]]},"references-count":48,"alternative-id":["10.1145\/3236024.3236049","10.1145\/3236024"],"URL":"https:\/\/doi.org\/10.1145\/3236024.3236049","relation":{},"subject":[],"published":{"date-parts":[[2018,10,26]]},"assertion":[{"value":"2018-10-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}