{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:23:58Z","timestamp":1750220638361,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":34,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,11,8]],"date-time":"2020-11-08T00:00:00Z","timestamp":1604793600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,11,8]]},"DOI":"10.1145\/3368089.3417938","type":"proceedings-article","created":{"date-parts":[[2020,11,8]],"date-time":"2020-11-08T06:03:47Z","timestamp":1604815427000},"page":"1541-1545","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["AlloyMC: Alloy meets model counting"],"prefix":"10.1145","author":[{"given":"Jiayi","family":"Yang","sequence":"first","affiliation":[{"name":"University of Texas at Austin, USA"}]},{"given":"Wenxi","family":"Wang","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, USA"}]},{"given":"Darko","family":"Marinov","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}]},{"given":"Sarfraz","family":"Khurshid","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, USA"}]}],"member":"320","published-online":{"date-parts":[[2020,11,8]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2010.27"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2006.75"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE.2010.11"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_15"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.2003.1238208"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36356-6_15"},{"key":"e_1_3_2_2_7_1","volume-title":"International Conference on Software Language Engineering. Springer, 102-122","author":"B\u0105k Kacper","year":"2010","unstructured":"Kacper B\u0105k , Krzysztof Czarnecki , and Andrzej W\u0105sowski . 2010 . Feature and metamodels in Clafer: mixed, specialized, and coupled . In International Conference on Software Language Engineering. Springer, 102-122 . Kacper B\u0105k, Krzysztof Czarnecki, and Andrzej W\u0105sowski. 2010. Feature and metamodels in Clafer: mixed, specialized, and coupled. In International Conference on Software Language Engineering. Springer, 102-122."},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/2832581.2832636"},{"volume-title":"Handbook of satisfiability","author":"Biere Armin","key":"e_1_3_2_2_9_1","unstructured":"Armin Biere , Marijn Heule , and Hans van Maaren . 2009. Handbook of satisfiability . Vol. 185 . IOS press . Armin Biere, Marijn Heule, and Hans van Maaren. 2009. Handbook of satisfiability. Vol. 185. IOS press."},{"key":"e_1_3_2_2_10_1","unstructured":"Armin Biere Marijn Heule Hans van Maaren and Toby Walsch. [n.d.]. Model Counting. 11.12. 1. Autarkies and qualitative matrix analysis ([n. d.]) 633.  Armin Biere Marijn Heule Hans van Maaren and Toby Walsch. [n.d.]. Model Counting. 11.12. 1. Autarkies and qualitative matrix analysis ([n. d.]) 633."},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-57288-8_9"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34281-3_16"},{"key":"e_1_3_2_2_13_1","first-page":"200","article-title":"A Scalable Approximate Model Counter","author":"Chakraborty Supratik","year":"2013","unstructured":"Supratik Chakraborty , Kuldeep S. Meel , and Moshe Y. Vardi . 2013 . A Scalable Approximate Model Counter . In Proc. of CP. 200 - 216 . Supratik Chakraborty, Kuldeep S. Meel, and Moshe Y. Vardi. 2013. A Scalable Approximate Model Counter. In Proc. of CP. 200-216.","journal-title":"Proc. of CP."},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"crossref","unstructured":"Carmel Domshlak and J\u00f6rg Hofmann. 2007. Probabilistic planning via heuristic forward search and weighted model counting. Journal of Artificial Intelligence Research 30 ( 2007 ) 565-620.  Carmel Domshlak and J\u00f6rg Hofmann. 2007. Probabilistic planning via heuristic forward search and weighted model counting. Journal of Artificial Intelligence Research 30 ( 2007 ) 565-620.","DOI":"10.1613\/jair.2289"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2019.00050"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606608"},{"key":"e_1_3_2_2_17_1","unstructured":"Carla P Gomes Ashish Sabharwal and Bart Selman. 2008. Model counting. ( 2008 ).  Carla P Gomes Ashish Sabharwal and Bart Selman. 2008. Model counting. ( 2008 )."},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/505145.505149"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87603-8_23"},{"key":"e_1_3_2_2_20_1","unstructured":"Vladimir Klebanov. 2012. Precise quantitative information flow analysis using symbolic model counting. QASA ( 2012 ).  Vladimir Klebanov. 2012. Precise quantitative information flow analysis using symbolic model counting. QASA ( 2012 )."},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"crossref","unstructured":"Jean-Marie Lagniez and Pierre Marquis. 2019. A Recursive Algorithm for Projected Model Counting. AAAI 33 ( 2019 ) 1536-1543.  Jean-Marie Lagniez and Pierre Marquis. 2019. A Recursive Algorithm for Projected Model Counting. AAAI 33 ( 2019 ) 1536-1543.","DOI":"10.1609\/aaai.v33i01.33011536"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1017584715408"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSNT.2011.141"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/2073876.2073922"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2590296.2590328"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(94)00092-1"},{"key":"e_1_3_2_2_27_1","first-page":"475","article-title":"Performing Bayesian inference by weighted model counting","volume":"5","author":"Sang Tian","year":"2005","unstructured":"Tian Sang , Paul Beame , and Henry A Kautz . 2005 . Performing Bayesian inference by weighted model counting . In AAAI , Vol. 5. 475 - 481 . Tian Sang, Paul Beame, and Henry A Kautz. 2005. Performing Bayesian inference by weighted model counting. In AAAI, Vol. 5. 475-481.","journal-title":"AAAI"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1512762.1512764"},{"volume-title":"Proceedings of AAAI Conference on Artificial Intelligence (AAAI).","author":"Soos Mate","key":"e_1_3_2_2_29_1","unstructured":"Mate Soos and Kuldeep S. Meel . 2019. BIRD: Engineering an Eficient CNF-XOR SAT Solver and its Applications to Approximate Model Counting . In Proceedings of AAAI Conference on Artificial Intelligence (AAAI). Mate Soos and Kuldeep S. Meel. 2019. BIRD: Engineering an Eficient CNF-XOR SAT Solver and its Applications to Approximate Model Counting. In Proceedings of AAAI Conference on Artificial Intelligence (AAAI)."},{"key":"e_1_3_2_2_30_1","first-page":"244","article-title":"Extending SAT Solvers to Cryptographic Problems","author":"Soos Mate","year":"2009","unstructured":"Mate Soos , Karsten Nohl , and Claude Castelluccia . 2009 . Extending SAT Solvers to Cryptographic Problems . In Theory and Applications of Satisfiability Testing (SAT). 244 - 257 . Mate Soos, Karsten Nohl, and Claude Castelluccia. 2009. Extending SAT Solvers to Cryptographic Problems. In Theory and Applications of Satisfiability Testing (SAT). 244-257.","journal-title":"Theory and Applications of Satisfiability Testing (SAT)."},{"key":"e_1_3_2_2_31_1","volume-title":"Kodkod: A Relational Model Finder. In TACAS.","author":"Torlak Emina","year":"2007","unstructured":"Emina Torlak and Daniel Jackson . 2007 . Kodkod: A Relational Model Finder. In TACAS. Emina Torlak and Daniel Jackson. 2007. Kodkod: A Relational Model Finder. In TACAS."},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2018.00081"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2010.30"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45190-5_7"}],"event":{"name":"ESEC\/FSE '20: 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"],"location":"Virtual Event USA","acronym":"ESEC\/FSE '20"},"container-title":["Proceedings of the 28th 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\/3368089.3417938","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3368089.3417938","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:01:59Z","timestamp":1750197719000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3368089.3417938"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,8]]},"references-count":34,"alternative-id":["10.1145\/3368089.3417938","10.1145\/3368089"],"URL":"https:\/\/doi.org\/10.1145\/3368089.3417938","relation":{},"subject":[],"published":{"date-parts":[[2020,11,8]]},"assertion":[{"value":"2020-11-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}