{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T03:19:58Z","timestamp":1782875998026,"version":"3.54.5"},"publisher-location":"New York, NY, USA","reference-count":61,"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":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-15-2-0087"],"award-info":[{"award-number":["FA8750-15-2-0087"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100008536","name":"Amazon Web Services","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100008536","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,10,26]]},"DOI":"10.1145\/3236024.3236064","type":"proceedings-article","created":{"date-parts":[[2018,10,29]],"date-time":"2018-10-29T12:06:00Z","timestamp":1540814760000},"page":"400-410","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":27,"title":["Parameterized model counting for string and numeric constraints"],"prefix":"10.1145","author":[{"given":"Abdulbaki","family":"Aydin","sequence":"first","affiliation":[{"name":"Microsoft, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"William","family":"Eiers","sequence":"additional","affiliation":[{"name":"University of California at Santa Barbara, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lucas","family":"Bang","sequence":"additional","affiliation":[{"name":"University of California at Santa Barbara, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tegan","family":"Brennan","sequence":"additional","affiliation":[{"name":"University of California at Santa Barbara, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Miroslav","family":"Gavrilov","sequence":"additional","affiliation":[{"name":"University of California at Santa Barbara, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tevfik","family":"Bultan","sequence":"additional","affiliation":[{"name":"University of California at Santa Barbara, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fang","family":"Yu","sequence":"additional","affiliation":[{"name":"National Chengchi University, Taiwan"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2018,10,26]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Parosh Aziz Abdulla Mohamed Faouzi Atig Yu-Fang Chen Luk\u00e1s Hol\u00edk Ahmed Rezine Philipp R\u00fcmmer and Jari Stenman. 2014.  Parosh Aziz Abdulla Mohamed Faouzi Atig Yu-Fang Chen Luk\u00e1s Hol\u00edk Ahmed Rezine Philipp R\u00fcmmer and Jari Stenman. 2014."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_10"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2610384.2610401"},{"key":"e_1_3_2_1_4_1","unstructured":"Abdulbaki Aydin. 2017.  Abdulbaki Aydin. 2017."},{"key":"e_1_3_2_1_5_1","unstructured":"Automata-based Model Counting String Constraint Solver for Vulnerability Analysis. dissertation. University of California Santa Barbara. https:\/\/www.alexandria.ucsb.edu\/lib\/ark:\/48907\/f3xp754k  Automata-based Model Counting String Constraint Solver for Vulnerability Analysis. dissertation. University of California Santa Barbara. https:\/\/www.alexandria.ucsb.edu\/lib\/ark:\/48907\/f3xp754k"},{"key":"e_1_3_2_1_6_1","volume-title":"CAV 2015, San Francisco, CA, USA, Proceedings, Part I. 255\u2013272","author":"Aydin Abdulbaki","year":"2015"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2009.18"},{"key":"e_1_3_2_1_8_1","volume-title":"ISSTAC: Integrated Symbolic Execution for Space-Time Analysis of Code. In submission.","author":"Balasubramanian Daniel","year":"2017"},{"key":"e_1_3_2_1_9_1","unstructured":"V. Baldoni N. Berline J.A. De Loera B. Dutra M. K\u00f6ppe S. Moreinis G. Pinto M. Vergne and J. Wu. {n. d.}. LattE integrale v1.7.2. http:\/\/www.math.ucdavis.edu\/ latte\/. ({n. d.}).  V. Baldoni N. Berline J.A. De Loera B. Dutra M. K\u00f6ppe S. Moreinis G. Pinto M. Vergne and J. Wu. {n. d.}. LattE integrale v1.7.2. http:\/\/www.math.ucdavis.edu\/ latte\/. ({n. d.})."},{"key":"e_1_3_2_1_10_1","unstructured":"Lucas Bang Abdulbaki Aydin Quoc-Sang Phan Corina S. P\u0103s\u0103reanu and Tevfik Bultan. 2016.  Lucas Bang Abdulbaki Aydin Quoc-Sang Phan Corina S. P\u0103s\u0103reanu and Tevfik Bultan. 2016."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950362"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054103001911"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1287\/moor.19.4.769"},{"key":"e_1_3_2_1_14_1","unstructured":"Mateus Borges Antonio Filieri Marcelo d\u2019Amorim and Corina S. Pasareanu. 2015.  Mateus Borges Antonio Filieri Marcelo d\u2019Amorim and Corina S. Pasareanu. 2015."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786832"},{"key":"e_1_3_2_1_16_1","unstructured":"Mateus Borges Quoc-Sang Phan Antonio Filieri and Corina S. Pasareanu. 2017.  Mateus Borges Quoc-Sang Phan Antonio Filieri and Corina S. Pasareanu. 2017."},{"key":"e_1_3_2_1_17_1","volume-title":"Approaches for Nonlinear Numerical Constraints. In Proceedings of the 9th International NASA Formal Methods Symposium. 131\u2013138","author":"Model-Counting"},{"key":"e_1_3_2_1_18_1","volume-title":"Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence. 1722\u20131730","author":"Chakraborty Supratik"},{"key":"e_1_3_2_1_19_1","unstructured":"Supratik Chakraborty Kuldeep S. Meel Rakesh Mistry and Moshe Y. Vardi. 2016.  Supratik Chakraborty Kuldeep S. Meel Rakesh Mistry and Moshe Y. Vardi. 2016."},{"key":"e_1_3_2_1_20_1","volume-title":"Word-Level Counting. In Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence. 3218\u20133224","author":"Approximate Probabilistic"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/2486788.2486870"},{"key":"e_1_3_2_1_22_1","unstructured":"Vijay Ganesh Mia Minnes Armando Solar-Lezama and Martin C. Rinard. 2012.  Vijay Ganesh Mia Minnes Armando Solar-Lezama and Martin C. Rinard. 2012."},{"key":"e_1_3_2_1_23_1","volume-title":"Proceedings of the 8th International Haifa Verification Conference (HVC). 209\u2013226","author":"Length Constraints Word Equations"},{"key":"e_1_3_2_1_24_1","unstructured":"Jaco Geldenhuys Matthew B. Dwyer and Willem Visser. 2012.  Jaco Geldenhuys Matthew B. Dwyer and Willem Visser. 2012."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2338965.2336773"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542498"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1858996.1859080"},{"key":"e_1_3_2_1_28_1","volume-title":"MD 20742","author":"Kelly Wayne","year":"1996"},{"key":"e_1_3_2_1_29_1","volume-title":"9th International Workshop, FSE 2002","author":"Kelsey John","year":"2002"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1572272.1572286"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/1018438.1021848"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.2"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03077-7_2"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2003.04.003"},{"key":"e_1_3_2_1_35_1","unstructured":"04\n   .003  04.003"},{"key":"e_1_3_2_1_36_1","unstructured":"Loi Luu Shweta Shinde Prateek Saxena and Brian Demsky. 2014.  Loi Luu Shweta Shinde Prateek Saxena and Brian Demsky. 2014."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594331"},{"key":"e_1_3_2_1_38_1","volume-title":"13th International Conference, CC 2004","author":"Parker Erin","year":"2004"},{"key":"e_1_3_2_1_39_1","unstructured":"Quoc-Sang Phan Pasquale Malacaria Corina S. Pasareanu and Marcelo d\u2019Amorim. 2014.  Quoc-Sang Phan Pasquale Malacaria Corina S. Pasareanu and Marcelo d\u2019Amorim. 2014."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2632362.2632367"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2382756.2382791"},{"key":"e_1_3_2_1_42_1","unstructured":"Bala Ravikumar and Gerry Eisman. 2004.  Bala Ravikumar and Gerry Eisman. 2004."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.07.009"},{"key":"e_1_3_2_1_44_1","unstructured":"Juliano Rizzo and Thai Duong. 2012.  Juliano Rizzo and Thai Duong. 2012."},{"key":"e_1_3_2_1_45_1","volume-title":"Security Conference).","author":"Ekoparty The CRIME"},{"key":"e_1_3_2_1_46_1","unstructured":"Prateek Saxena Devdatta Akhawe Steve Hanna Feng Mao Stephen McCamant and Dawn Song. 2010.  Prateek Saxena Devdatta Akhawe Steve Hanna Feng Mao Stephen McCamant and Dawn Song. 2010."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.38"},{"key":"e_1_3_2_1_48_1","volume-title":"12th International Conference, FOSSACS 2009, York, UK, March 22-29, 2009. Proceedings. 288\u2013302","author":"Smith Geoffrey","year":"2009"},{"key":"e_1_3_2_1_49_1","unstructured":"Richard P. Stanley. 2011.  Richard P. Stanley. 2011."},{"key":"e_1_3_2_1_50_1","unstructured":"Enumerative Combinatorics: Volume 1 (2nd ed.). Cambridge University Press New York NY USA.   Enumerative Combinatorics: Volume 1 (2nd ed.). Cambridge University Press New York NY USA."},{"key":"e_1_3_2_1_51_1","unstructured":"Cesare Tinelli Clark Barrett Morgan Deters Tianyi Liang Andrew Reynolds. 2014.  Cesare Tinelli Clark Barrett Morgan Deters Tianyi Liang Andrew Reynolds. 2014."},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_43"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660372"},{"key":"e_1_3_2_1_54_1","unstructured":"Minh-Thai Trinh Duc-Hiep Chu and Joxan Jaffar. 2017.  Minh-Thai Trinh Duc-Hiep Chu and Joxan Jaffar. 2017."},{"key":"e_1_3_2_1_55_1","volume-title":"CAV 2017, Heidelberg, Germany, Proceedings, Part II. 399\u2013418","author":"Recursively-Defined Strings Model Counting"},{"key":"e_1_3_2_1_56_1","unstructured":"Fang Yu Muath Alkhalaf and Tevfik Bultan. 2009.  Fang Yu Muath Alkhalaf and Tevfik Bultan. 2009."},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2009.20"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-013-0189-1"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_28"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054111009112"},{"key":"e_1_3_2_1_61_1","unstructured":"Yunhui Zheng Xiangyu Zhang and Vijay Ganesh. 2013.  Yunhui Zheng Xiangyu Zhang and Vijay Ganesh. 2013."}],"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.3236064","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3236024.3236064","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3236024.3236064","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.3236064"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10,26]]},"references-count":61,"alternative-id":["10.1145\/3236024.3236064","10.1145\/3236024"],"URL":"https:\/\/doi.org\/10.1145\/3236024.3236064","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"}}]}}