{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T23:02:47Z","timestamp":1743030167868,"version":"3.40.3"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030636173"},{"type":"electronic","value":"9783030636180"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-63618-0_8","type":"book-chapter","created":{"date-parts":[[2020,12,5]],"date-time":"2020-12-05T08:04:14Z","timestamp":1607155454000},"page":"124-143","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["MCBAT: Model Counting for Constraints over Bounded Integer Arrays"],"prefix":"10.1007","author":[{"given":"Abtin","family":"Molavi","sequence":"first","affiliation":[]},{"given":"Tommy","family":"Schneider","sequence":"additional","affiliation":[]},{"given":"Mara","family":"Downing","sequence":"additional","affiliation":[]},{"given":"Lucas","family":"Bang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,12,6]]},"reference":[{"key":"8_CR1","volume-title":"Solvable Cases of the Decision Problem","author":"W Ackermann","year":"1954","unstructured":"Ackermann, W.: Solvable Cases of the Decision Problem. North-Holland Pub. Co., Amsterdam (1954)"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/978-3-319-21690-4_15","volume-title":"Computer Aided Verification","author":"A Aydin","year":"2015","unstructured":"Aydin, A., Bang, L., Bultan, T.: Automata-based model counting for string constraints. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 255\u2013272. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_15"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Aydin, A., et al.: Parameterized model counting for string and numeric constraints. In: Proceedings of the 2018 ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC\/SIGSOFT FSE 2018, Lake Buena Vista, FL, USA, 04\u201309 November 2018, pp. 400\u2013410 (2018)","DOI":"10.1145\/3236024.3236064"},{"issue":"4","key":"8_CR4","doi-asserted-by":"publisher","first-page":"769","DOI":"10.1287\/moor.19.4.769","volume":"19","author":"AI Barvinok","year":"1994","unstructured":"Barvinok, A.I.: A polynomial time algorithm for counting integral points in polyhedra when the dimension is fixed. Math. Oper. Res. 19(4), 769\u2013779 (1994)","journal-title":"Math. Oper. Res."},{"key":"8_CR5","unstructured":"Belle, V.: Weighted model counting with function symbols. In: Proceedings of the Thirty-Third Conference on Uncertainty in Artificial Intelligence, UAI 2017, Sydney, Australia, 11\u201315 August 2017 (2017)"},{"key":"8_CR6","unstructured":"Birnbaum, E., Lozinskii, E.L.: The good old Davis-Putnam procedure helps counting models. J. Artif. Int. Res. 10(1), 457\u2013477 (1999)"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-319-57288-8_9","volume-title":"NASA Formal Methods","author":"M Borges","year":"2017","unstructured":"Borges, M., Phan, Q.-S., Filieri, A., P\u0103s\u0103reanu, C.S.: Model-counting approaches for nonlinear numerical constraints. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 131\u2013138. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-57288-8_9"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/11609773_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427\u2013442. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11609773_28"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Meel, K., Mistry, R., Vardi, M.: Approximate probabilistic inference via word-level counting, November 2015","DOI":"10.1609\/aaai.v30i1.10416"},{"issue":"6","key":"8_CR10","doi-asserted-by":"publisher","first-page":"772","DOI":"10.1016\/j.artint.2007.11.002","volume":"172","author":"M Chavira","year":"2008","unstructured":"Chavira, M., Darwiche, A.: On probabilistic inference by weighted model counting. Artif. Intell. 172(6), 772\u2013799 (2008)","journal-title":"Artif. Intell."},{"key":"8_CR11","unstructured":"De Salvo Braz, R., O\u2019Reilly, C., Gogate, V., Dechter, R.: Probabilistic inference modulo theories. In: Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, pp. 3591\u20133599. AAAI Press (2016)"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Eiers, W., Saha, S., Brennan, T., Bultan, T.: Subformula caching for model counting and quantitative program analysis. In: Proceedings of The 34th IEEE\/ACM International Conference on Automated Software Engineering ASE (2019)","DOI":"10.1109\/ASE.2019.00050"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/978-3-319-23404-5_15","volume-title":"Model Checking Software","author":"A Filieri","year":"2015","unstructured":"Filieri, A., Frias, M.F., P\u0103s\u0103reanu, C.S., Visser, W.: Model counting for complex data structures. In: Fischer, B., Geldenhuys, J. (eds.) SPIN 2015. LNCS, vol. 9232, pp. 222\u2013241. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23404-5_15"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Filieri, A., Pasareanu, C.S., Visser, W.: Reliability analysis in symbolic pathfinder. In: 35th International Conference on Software Engineering, ICSE 2013, San Francisco, CA, USA, 18\u201326 May 2013, pp. 622\u2013631 (2013)","DOI":"10.1109\/ICSE.2013.6606608"},{"issue":"1","key":"8_CR15","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/0304-3975(91)90145-R","volume":"79","author":"P Flajolet","year":"1991","unstructured":"Flajolet, P., Salvy, B., Zimmermann, P.: Automatic average-case analysis of algorithm. Theor. Comput. Sci. 79(1), 37\u2013109 (1991)","journal-title":"Theor. Comput. Sci."},{"issue":"6","key":"8_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3011286.3011296","volume":"41","author":"A Fromherz","year":"2016","unstructured":"Fromherz, A., Luckow, K.S., Pasareanu, C.S.: Symbolic arrays in symbolic pathfinder. ACM SIGSOFT Softw. Eng. Notes 41(6), 1\u20135 (2016)","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Geldenhuys, J., Dwyer, M.B., Visser, W.: Probabilistic symbolic execution. In: Proceedings of the 2012 International Symposium on Software Testing and Analysis, ISSTA 2012, pp. 166\u2013176. ACM, New York (2012)","DOI":"10.1145\/2338965.2336773"},{"key":"8_CR18","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1016\/j.tcs.2014.04.022","volume":"538","author":"V Klebanov","year":"2014","unstructured":"Klebanov, V.: Precise quantitative information flow analysis - a symbolic approach. Theor. Comput. Sci. 538, 124\u2013139 (2014)","journal-title":"Theor. Comput. Sci."},{"key":"8_CR19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74105-3","volume-title":"Decision Procedures: An Algorithmic Point of View","author":"D Kroening","year":"2008","unstructured":"Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View, 1st edn. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-74105-3","edition":"1"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-642-35873-9_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D Larraz","year":"2013","unstructured":"Larraz, D., Rodr\u00edguez-Carbonell, E., Rubio, A.: SMT-based array invariant generation. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 169\u2013188. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35873-9_12"},{"issue":"4","key":"8_CR21","doi-asserted-by":"publisher","first-page":"1273","DOI":"10.1016\/j.jsc.2003.04.003","volume":"38","author":"JAD Loera","year":"2004","unstructured":"Loera, J.A.D., Hemmecke, R., Tauzer, J., Yoshida, R.: Effective lattice point counting in rational convex polytopes. J. Symb. Comput. 38(4), 1273\u20131302 (2004)","journal-title":"J. Symb. Comput."},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Luu, L., Shinde, S., Saxena, P., Demsky, B.: A model counter for constraints over unbounded strings. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014, pp. 565\u2013576. ACM, New York (2014)","DOI":"10.1145\/2594291.2594331"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Malacaria, P., Khouzani, M.H.R., Pasareanu, C.S., Phan, Q., Luckow, K.S.: Symbolic side-channel analysis for probabilistic programs. In: 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, 9\u201312 July 2018, pp. 313\u2013327 (2018)","DOI":"10.1109\/CSF.2018.00030"},{"key":"8_CR24","series-title":"Studies in Cognitive Systems","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-94-011-1793-7_2","volume-title":"Information Processing","author":"J McCarthy","year":"1962","unstructured":"McCarthy, J.: Towards a mathematical science of computation. In: Colburn, T.R., Fetzer, J.H., Rankin, T.L. (eds.) Information Processing. SCS, vol. 14, pp. 21\u201328. Springer, Dordrecht (1962). https:\/\/doi.org\/10.1007\/978-94-011-1793-7_2"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient smt solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Generalized, efficient array decision procedures. In: Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, 15\u201318 November 2009, Austin, Texas, USA pp. 45\u201352 (2009)","DOI":"10.1109\/FMCAD.2009.5351142"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"Phan, Q., Malacaria, P., Pasareanu, C.S., d\u2019Amorim, M.: Quantifying information leaks using reliability analysis. In: 2014 International Symposium on Model Checking of Software, SPIN 2014, Proceedings, San Jose, CA, USA, 21\u201323 July 2014, pp. 105\u2013108 (2014)","DOI":"10.1145\/2632362.2632367"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"Plazar, Q., Acher, M., Bardin, S., Gotlieb, A.: Efficient and complete fd-solving for extended array constraints, pp. 1231\u20131238, August 2017","DOI":"10.24963\/ijcai.2017\/171"},{"key":"8_CR29","doi-asserted-by":"crossref","unstructured":"Pugh, W.: Counting solutions to Presburger formulas: how and why. In: Proceedings of the ACM SIGPLAN 1994 Conference on Programming Language Design and Implementation, PLDI 1994, pp. 121\u2013134. ACM, New York (1994)","DOI":"10.1145\/773473.178254"},{"key":"8_CR30","unstructured":"Sang, T., Bearne, P., Kautz, H.: Performing bayesian inference by weighted model counting. In: Proceedings of the 20th National Conference on Artificial Intelligence, AAAI 2005, vol. 1, pp. 475\u2013481. AAAI Press (2005)"},{"key":"8_CR31","doi-asserted-by":"crossref","unstructured":"Sherman, E., Harris, A.: Accurate string constraints solution counting with weighted automata. In: Proceedings of The 34th IEEE\/ACM International Conference on Automated Software Engineering ASE (2019)","DOI":"10.1109\/ASE.2019.00049"},{"key":"8_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/978-3-319-63390-9_21","volume-title":"Computer Aided Verification","author":"M-T Trinh","year":"2017","unstructured":"Trinh, M.-T., Chu, D.-H., Jaffar, J.: Model counting for recursively-defined strings. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 399\u2013418. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_21"},{"key":"8_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1007\/978-3-030-01090-4_24","volume-title":"Automated Technology for Verification and Analysis","author":"N Tsiskaridze","year":"2018","unstructured":"Tsiskaridze, N., Bang, L., McMahan, J., Bultan, T., Sherwood, T.: Information leakage in arbiter protocols. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 404\u2013421. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_24"},{"key":"8_CR34","doi-asserted-by":"crossref","unstructured":"Verdoolaege, S., Seghir, R., Beyls, K., Loechner, V., Bruynooghe, M.: Counting integer points in parametric polytopes using Barvinok\u2019s rational functions. Algorithmica 48(1), 37\u201366 (2007)","DOI":"10.1007\/s00453-006-1231-0"},{"key":"8_CR35","unstructured":"Visser, W., Pasareanu, C.S.: Probabilistic programming for Java using symbolic execution and model counting. In: Proceedings of the South African Institute of Computer Scientists and Information Technologists, SAICSIT 2017, Thaba Nchu, South Africa, 26\u201328 September 2017, pp. 35:1\u201335:10 (2017)"}],"container-title":["Lecture Notes in Computer Science","Software Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-63618-0_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,14]],"date-time":"2023-10-14T17:18:46Z","timestamp":1697303926000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-63618-0_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030636173","9783030636180"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-63618-0_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"6 December 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VSTTE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Working Conference on Verified Software: Theories, Tools, and Experiments","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Los Angeles, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vstte2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sri-csl.github.io\/VSTTE20\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"57% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Due to COVID-19 pandemic the conference was held virtually","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}