{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T01:42:12Z","timestamp":1769737332542,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":59,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,12,21]],"date-time":"2020-12-21T00:00:00Z","timestamp":1608508800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100006435","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1718903"],"award-info":[{"award-number":["CCF-1718903"]}],"id":[{"id":"10.13039\/100006435","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,12,21]]},"DOI":"10.1145\/3324884.3416563","type":"proceedings-article","created":{"date-parts":[[2021,1,27]],"date-time":"2021-01-27T23:39:02Z","timestamp":1611790742000},"page":"709-721","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["TestMC"],"prefix":"10.1145","author":[{"given":"Muhammad","family":"Usman","sequence":"first","affiliation":[{"name":"University of Texas at Austin"}]},{"given":"Wenxi","family":"Wang","sequence":"additional","affiliation":[{"name":"University of Texas at Austin"}]},{"given":"Sarfraz","family":"Khurshid","sequence":"additional","affiliation":[{"name":"University of Texas at Austin"}]}],"member":"320","published-online":{"date-parts":[[2021,1,27]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2019. Alloy 4 Download Webpage. http:\/\/alloy.lcs.mit.edu\/alloy\/download.html."},{"key":"e_1_3_2_1_2_1","volume-title":"Test Case Minimization Approach Using Fault Detection and Combinatorial Optimization Techniques for Configuration-Aware Structural Testing. Journal of Engineering Science and Technology 12 (05","author":"Ahmed Bestoun","year":"2016","unstructured":"Bestoun Ahmed. 2016. Test Case Minimization Approach Using Fault Detection and Combinatorial Optimization Techniques for Configuration-Aware Structural Testing. Journal of Engineering Science and Technology 12 (05 2016), 737--753."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"crossref","unstructured":"\u00d6zg\u00fcr Akg\u00fcn Ian P. Gent Christopher Jefferson Ian Miguel and Peter Nightingale. 2018. Metamorphic Testing of Constraint Solvers. In Principles and Practice of Constraint Programming. 727--736.","DOI":"10.1007\/978-3-319-98334-9_46"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Cyrille Artho Armin Biere and Martina Seidl. 2013. Model-Based Testing for Verification Back-Ends. In Tests and Proofs. 39--55.","DOI":"10.1007\/978-3-642-38916-0_3"},{"key":"e_1_3_2_1_5_1","volume-title":"Model-Based Testing of Stateful APIs with Modbat. 30th IEEE\/ACM International Conference on Automated Software Engineering (ASE)","author":"Artho Cyrille","year":"2015","unstructured":"Cyrille Artho, Martina Seidl, Quentin Gros, Eun-Hye Choi, Takashi Kitamura, Akira Mori, Rudolf Ramler, and Yoriyuki Yamagata. 2015. Model-Based Testing of Stateful APIs with Modbat. 30th IEEE\/ACM International Conference on Automated Software Engineering (ASE) (2015), 858--863."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"crossref","unstructured":"Cyrille Valentin Artho Armin Biere Masami Hagiya Eric Platon Martina Seidl Yoshinori Tanabe and Mitsuharu Yamamoto. 2013. ModBat: A Model-Based API Tester for Event-Driven Systems. In Hardware and Software: Verification and Testing Valeria Bertacco and Axel Legay (Eds.). 112--128.","DOI":"10.1007\/978-3-319-03077-7_8"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Abdulbaki Aydin Lucas Bang and Tevfik Bultan. 2015. Automata-Based Model Counting for String Constraints. In Computer Aided Verification. 255--272.","DOI":"10.1007\/978-3-319-21690-4_15"},{"key":"e_1_3_2_1_8_1","volume-title":"Stuckey","author":"Aziz Rehan Abdul","year":"2015","unstructured":"Rehan Abdul Aziz, Geoffrey Chu, Christian J. Muise, and Peter J. Stuckey. 2015. #∃SAT: Projected Model Counting. In SAT."},{"key":"e_1_3_2_1_9_1","unstructured":"Fahiem Bacchus and Toby Walsh. 2005. A non-CNF DIMACS style."},{"key":"e_1_3_2_1_11_1","volume-title":"Picosat essentials. Journal on Satisfiability, Boolean Modeling and Computation (JSAT ([n. d.])","author":"Biere Armin","year":"2008","unstructured":"Armin Biere. [n.d.]. Picosat essentials. Journal on Satisfiability, Boolean Modeling and Computation (JSAT ([n. d.]), 2008."},{"key":"e_1_3_2_1_12_1","unstructured":"A. Biere A. Biere M. Heule H. van Maaren and T. Walsh. 2009. Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications."},{"key":"e_1_3_2_1_13_1","first-page":"24","article-title":"SMT Solvers: Foundations and Applications","volume":"45","author":"Bj\u00f8rner Nikolaj","year":"2016","unstructured":"Nikolaj Bj\u00f8rner. 2016. SMT Solvers: Foundations and Applications. Dependable Software Systems Engineering 45 (2016), 24.","journal-title":"Dependable Software Systems Engineering"},{"key":"e_1_3_2_1_14_1","volume-title":"StringFuzz: A Fuzzer for String Solvers","author":"Blotsky Dmitry","unstructured":"Dmitry Blotsky, Federico Mora, Murphy Berzish, Yunhui Zheng, Ifaz Kabir, and Vijay Ganesh. 2018. StringFuzz: A Fuzzer for String Solvers. In Computer Aided Verification, Hana Chockler and Georg Weissenbacher (Eds.). Springer International Publishing, Cham, 45--51."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1670412.1670413"},{"key":"e_1_3_2_1_16_1","volume-title":"Testing and Debugging Techniques for Answer Set Solver Development. CoRR abs\/1007.3223","author":"Brummayer Robert","year":"2010","unstructured":"Robert Brummayer and Matti J\u00e4rvisalo. 2010. Testing and Debugging Techniques for Answer Set Solver Development. CoRR abs\/1007.3223 (2010). arXiv:1007.3223 http:\/\/arxiv.org\/abs\/1007.3223"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14186-7_6"},{"key":"e_1_3_2_1_18_1","volume-title":"Proceedings of International Joint Conference on Artificial Intelligence (IJCAI).","author":"Chakraborty Supratik","unstructured":"Supratik Chakraborty, Kuldeep S. Meel, and Moshe Y. Vardi. 2016. Algorithmic Improvements in Approximate Counting for Probabilistic Inference: From Linear to Logarithmic SAT Calls. In Proceedings of International Joint Conference on Artificial Intelligence (IJCAI)."},{"key":"e_1_3_2_1_19_1","volume-title":"Model-Based Coverage-Driven Test Suite Generation for Software Product Lines","author":"Cichos Harald","unstructured":"Harald Cichos, Sebastian Oster, Malte Lochau, and Andy Sch\u00fcrr. 2011. Model-Based Coverage-Driven Test Suite Generation for Software Product Lines. In Model Driven Engineering Languages and Systems, Jon Whittle, Tony Clark, and Thomas K\u00fchne (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 425--439."},{"key":"e_1_3_2_1_20_1","volume-title":"Peled","author":"Clarke Edmund M.","year":"1999","unstructured":"Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled. 1999. Model Checking. MIT Press."},{"key":"e_1_3_2_1_21_1","volume-title":"A Framework for the Specification of Random SAT and QSAT Formulas","author":"Creignou Nadia","unstructured":"Nadia Creignou, Uwe Egly, and Martina Seidl. 2012. A Framework for the Specification of Random SAT and QSAT Formulas. In Tests and Proofs, Achim D. Brucker and Jacques Julliand (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 163--168."},{"key":"e_1_3_2_1_22_1","volume-title":"On the tractable counting of theory models and its application to belief revision and truth maintenance. CoRR cs.AI\/0003044","author":"Darwiche Adnan","year":"2000","unstructured":"Adnan Darwiche. 2000. On the tractable counting of theory models and its application to belief revision and truth maintenance. CoRR cs.AI\/0003044 (2000). http:\/\/arxiv.org\/abs\/cs.AI\/0003044"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"e_1_3_2_1_24_1","volume-title":"Probabilistic Planning via Heuristic Forward Search and Weighted Model Counting. CoRR abs\/1111.0044","author":"Domshlak Carmel","year":"2011","unstructured":"Carmel Domshlak and J\u00f6rg Hoffmann. 2011. Probabilistic Planning via Heuristic Forward Search and Weighted Model Counting. CoRR abs\/1111.0044 (2011). arXiv:1111.0044 http:\/\/arxiv.org\/abs\/1111.0044"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236057"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"crossref","unstructured":"Antonio Filieri Corina S. P\u0103s\u0103reanu and Willem Visser. 2013. Reliability Analysis in Symbolic Pathfinder. In ICSE. 622--631.","DOI":"10.1109\/ICSE.2013.6606608"},{"key":"e_1_3_2_1_27_1","volume-title":"Constraint Solver. In Proceedings of the 2006 Conference on ECAI 2006: 17th European Conference on Artificial Intelligence August 29 --","author":"Gent Ian P.","year":"2006","unstructured":"Ian P. Gent, Chris Jefferson, and Ian Miguel. 2006. MINION: A Fast, Scalable, Constraint Solver. In Proceedings of the 2006 Conference on ECAI 2006: 17th European Conference on Artificial Intelligence August 29 -- September 1, 2006, Riva Del Garda, Italy. IOS Press, Amsterdam, The Netherlands, The Netherlands, 98--102. http:\/\/dl.acm.org\/citation.cfm?id=1567016.1567043"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-SEIP.2019.00016"},{"key":"e_1_3_2_1_29_1","volume-title":"DLFuzz: Differential Fuzzing Testing of Deep Learning Systems. CoRR abs\/1808.09413","author":"Guo Jianmin","year":"2018","unstructured":"Jianmin Guo, Yu Jiang, Yue Zhao, Quan Chen, and Jiaguang Sun. 2018. DLFuzz: Differential Fuzzing Testing of Deep Learning Systems. CoRR abs\/1808.09413 (2018). arXiv:1808.09413 http:\/\/arxiv.org\/abs\/1808.09413"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050043"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/505145.505149"},{"key":"e_1_3_2_1_32_1","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"Jackson Daniel","year":"2012","unstructured":"Daniel Jackson. 2012. Software Abstractions: Logic, Language, and Analysis. The MIT Press."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-018-9600-2"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v33i01.33011536"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236037"},{"key":"e_1_3_2_1_36_1","first-page":"100","article-title":"Differential Testing for Software","volume":"10","author":"McKeeman William M.","year":"1998","unstructured":"William M. McKeeman. 1998. Differential Testing for Software. DIGITAL TECHNICAL JOURNAL 10, 1 (1998), 100--107.","journal-title":"DIGITAL TECHNICAL JOURNAL"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30353-1_36"},{"key":"e_1_3_2_1_38_1","volume-title":"Proceedings of the National Conference on Artificial Intelligence 1, 436--442","author":"Navarro P\u00e9rez Juan Antonio","year":"2005","unstructured":"Juan Antonio Navarro P\u00e9rez and Andrei Voronkov. 2005. Generation of Hard Non-Clausal Random Satisfiability Problems. Proceedings of the National Conference on Artificial Intelligence 1, 436--442."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884836"},{"key":"e_1_3_2_1_40_1","first-page":"53","article-title":"Boolector 2.0","volume":"9","author":"Niemetz Aina","year":"2014","unstructured":"Aina Niemetz, Mathias Preiner, and Armin Biere. 2014. Boolector 2.0. JSAT 9 (2014), 53--58.","journal-title":"JSAT"},{"key":"e_1_3_2_1_41_1","unstructured":"Aina Niemetz Mathias Preiner and Armin Biere. 2017. MODEL-BASED API TESTING FOR SMT SOLVERS."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30201-8_33"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2017.62"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2590296.2590328"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(94)00092-1"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.1566"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2016.2532875"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2019\/163"},{"key":"e_1_3_2_1_49_1","volume-title":"CryptoMiniSat v4. SAT Competition","author":"Soos Mate","year":"2014","unstructured":"Mate Soos. 2014. CryptoMiniSat v4. SAT Competition (2014), 23."},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1013886.1007531"},{"key":"e_1_3_2_1_51_1","volume-title":"Gecode: Generic constraint development environment","author":"Team Gecode","year":"2006","unstructured":"Gecode Team. 2006. Gecode: Generic constraint development environment. http:\/\/www.gecode.org"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814948_38"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386015"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.456"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"crossref","unstructured":"Wenxi Wang Muhammad Usman Alyas Almaawi Kaiyuan Wang Kuldeep S. Meel and Sarfraz Khurshid. 2020. A Study of Symmetry Breaking Predicates and Model Counting. In TACAS.","DOI":"10.1007\/978-3-030-45190-5_7"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2017.2655056"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48166-4_16"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.988498"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.988498"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338906.3338932"}],"event":{"name":"ASE '20: 35th IEEE\/ACM International Conference on Automated Software Engineering","location":"Virtual Event Australia","acronym":"ASE '20","sponsor":["SIGAI ACM Special Interest Group on Artificial Intelligence","SIGSOFT ACM Special Interest Group on Software Engineering","IEEE CS"]},"container-title":["Proceedings of the 35th IEEE\/ACM International Conference on Automated Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3324884.3416563","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3324884.3416563","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:01:38Z","timestamp":1750197698000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3324884.3416563"}},"subtitle":["testing model counters using differential and metamorphic testing"],"short-title":[],"issued":{"date-parts":[[2020,12,21]]},"references-count":59,"alternative-id":["10.1145\/3324884.3416563","10.1145\/3324884"],"URL":"https:\/\/doi.org\/10.1145\/3324884.3416563","relation":{},"subject":[],"published":{"date-parts":[[2020,12,21]]},"assertion":[{"value":"2021-01-27","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}