{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:43:00Z","timestamp":1773193380216,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":33,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,6,11]],"date-time":"2020-06-11T00:00:00Z","timestamp":1591833600000},"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,6,11]]},"DOI":"10.1145\/3385412.3385985","type":"proceedings-article","created":{"date-parts":[[2020,6,7]],"date-time":"2020-06-07T01:40:10Z","timestamp":1591494010000},"page":"718-730","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":69,"title":["Validating SMT solvers via semantic fusion"],"prefix":"10.1145","author":[{"given":"Dominik","family":"Winterer","sequence":"first","affiliation":[{"name":"ETH Zurich, Switzerland"}]},{"given":"Chengyu","family":"Zhang","sequence":"additional","affiliation":[{"name":"East China Normal University, China"}]},{"given":"Zhendong","family":"Su","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}]}],"member":"320","published-online":{"date-parts":[[2020,6,11]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"10","volume":"201","author":"Compiler Using","unstructured":"2019. Using the GNU Compiler Collection (GCC): Gcov. Retrieved 2019-10-30 from https:\/\/gcc.gnu.org\/onlinedocs\/gcc\/Gcov.html","journal-title":"Gcov. Retrieved"},{"key":"e_1_3_2_1_2_1","unstructured":"Clark Barrett Christopher L. Conway Morgan Deters Liana Hadarean Dejan Jovanovi\u0107 Tim King Andrew Reynolds and Cesare Tinelli. 2011."},{"key":"e_1_3_2_1_3_1","unstructured":"CVC4. In CAV. 171\u2013177."},{"key":"e_1_3_2_1_4_1","unstructured":"Clark Barrett Pascal Fontaine and Cesare Tinelli. 2019. The Satisfiability Modulo Theories Library (SMT-LIB). Retrieved 2019-10-30 from www.SMT-LIB.org"},{"key":"e_1_3_2_1_5_1","unstructured":"Clark Barrett Aaron Stump and Cesare Tinelli. 2010. The SMT-LIB Standard: Version 2.0. In SMT."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"crossref","unstructured":"Dmitry Blotsky Federico Mora Murphy Berzish Yunhui Zheng Ifaz Kabir and Vijay Ganesh. 2018. StringFuzz: A fuzzer for string solvers. In CAV. 45\u201351.","DOI":"10.1007\/978-3-319-96142-2_6"},{"key":"e_1_3_2_1_7_1","volume-title":"Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays. In TACAS. 174\u2013177.","author":"Brummayer Robert","year":"2009","unstructured":"Robert Brummayer and Armin Biere. 2009. Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays. In TACAS. 174\u2013177."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Robert Brummayer and Armin Biere. 2009. Fuzzing and deltadebugging SMT solvers. In SMT. 1\u20135.","DOI":"10.1145\/1670412.1670413"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"crossref","unstructured":"Robert Brummayer Florian Lonsing and Armin Biere. 2010. Automated Testing and Debugging of SAT and QBF Solvers. In SAT. 44\u201357.","DOI":"10.1007\/978-3-642-14186-7_6"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","unstructured":"Alexandra Bugariu and Peter M\u00fcller. 2020. Automatically Testing String Solvers. In ICSE. 10.3929\/ethz-b-000375243","DOI":"10.3929\/ethz-b-000375243"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Alexandra Bugariu Valentin W\u00fcstholz Maria Christakis and Peter M\u00fcller. 2018. Automatically testing implementations of numerical abstract domains. In ASE. 768\u2013778.","DOI":"10.1145\/3238147.3240464"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"crossref","unstructured":"Cristian Cadar and Alastair Donaldson. 2016. Analysing the Program Analyser. In ICSE. 765\u2013768.","DOI":"10.1145\/2889160.2889206"},{"key":"e_1_3_2_1_13_1","volume-title":"Engler","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar, Daniel Dunbar, and Dawson R. Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In OSDI. 209\u2013224."},{"key":"e_1_3_2_1_15_1","unstructured":"The International SMT Competition. 2019. SMT-COMP. Retrieved 2019-10-30 from https:\/\/smt-comp.github.io\/2019\/index.html"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"crossref","unstructured":"Leonardo de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In TACAS.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_18_1","volume-title":"Saxe","author":"Detlefs David","year":"2005","unstructured":"David Detlefs, Greg Nelson, and James B. Saxe. 2005. Simplify: A Theorem Prover for Program Checking. JACM (2005), 365\u2013473."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Alastair F Donaldson Hugues Evrard Andrei Lascu and Paul Thomson. 2017. Automated testing of graphics shader compilers. In OOPSLA.","DOI":"10.1145\/3133917"},{"key":"e_1_3_2_1_20_1","unstructured":"Vijay Ganesh Dmitry Blotsky Federico Mora Ifaz Kabir Murphy Berzish and Yunhui Zheng. 2019. StringFuzz. Retrieved 2019-10-30 from http:\/\/stringfuzz.dmitryblotsky.com\/"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Patrice Godefroid Nils Klarlund and Koushik Sen. 2005. DART: directed automated random testing. In PLDI. 213\u2013223.","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"crossref","unstructured":"Timotej Kapus and Cristian Cadar. 2017. Automatic testing of symbolic execution engines via program generation and differential testing. In ASE. 590\u2013600.","DOI":"10.1109\/ASE.2017.8115669"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"crossref","unstructured":"Christian Klinger Maria Christakis and Valentin W\u00fcstholz. 2019. Differentially testing soundness and precision of program analyzers. In ISSTA. 239\u2013250.","DOI":"10.1145\/3293882.3330553"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"crossref","unstructured":"Vu Le Mehrdad Afshari and Zhendong Su. 2014. Compiler validation via equivalence modulo inputs. In PLDI. 216\u2013226.","DOI":"10.1145\/2594291.2594334"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"crossref","unstructured":"Vu Le Chengnian Sun and Zhendong Su. 2015. Finding deep compiler bugs via guided stochastic program mutation. In OOPSLA. 386\u2013399.","DOI":"10.1145\/2814270.2814319"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"crossref","unstructured":"Christopher Lidbury Andrei Lascu Nathan Chong and Alastair F Donaldson. 2015. Many-core compiler fuzzing. In PLDI. 65\u201376.","DOI":"10.1145\/2737924.2737986"},{"key":"e_1_3_2_1_27_1","unstructured":"Aina Niemetz Mathias Preiner and Armin Biere. 2017. Model-based API testing for SMT solvers. In SMT."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"crossref","unstructured":"Felix Pauck Eric Bodden and Heike Wehrheim. 2018. Do Android taint analysis tools keep their promises?. In ESEC\/FSE. 331\u2013341.","DOI":"10.1145\/3236024.3236029"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"crossref","unstructured":"Lina Qiu Yingying Wang and Julia Rubin. 2018. Analyzing the analyzers: FlowDroid\/IccTA AmanDroid and DroidSafe. In ISSTA. 176\u2013186.","DOI":"10.1145\/3213846.3213873"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"crossref","unstructured":"John Regehr Yang Chen Pascal Cuoq Eric Eide Chucky Ellison and Xuejun Yang. 2012. Test-case Reduction for C Compiler Bugs. In PLDI. 335\u2013346.","DOI":"10.1145\/2254064.2254104"},{"key":"e_1_3_2_1_31_1","volume-title":"A survey on metamorphic testing. TSE","author":"Segura Sergio","year":"2016","unstructured":"Sergio Segura, Gordon Fraser, Ana B Sanchez, and Antonio Ruiz-Cort\u00e9s. 2016. A survey on metamorphic testing. TSE (2016), 805\u2013824."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"crossref","unstructured":"Chengnian Sun Vu Le and Zhendong Su. 2016. Finding compiler bugs via live code mutation. In OOPSLA. 849\u2013863.","DOI":"10.1145\/2983990.2984038"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"crossref","unstructured":"Emina Torlak and Rastislav Bodik. 2014. A lightweight symbolic virtual machine for solver-aided host languages. In PLDI. 530\u2013541.","DOI":"10.1145\/2594291.2594340"},{"key":"e_1_3_2_1_35_1","unstructured":"Jingyue Wu Gang Hu Yang Tang and Junfeng Yang. 2013. Effective dynamic detection of alias analysis errors. In ESEC\/FSE. 279\u2013289."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"crossref","unstructured":"Chengyu Zhang Ting Su Yichen Yan Fuyuan Zhang Geguang Pu and Zhendong Su. 2019. Finding and understanding bugs in software model checkers. In ESEC\/FSE. 763\u2013773.","DOI":"10.1145\/3338906.3338932"}],"event":{"name":"PLDI '20: 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation","location":"London UK","acronym":"PLDI '20","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3385412.3385985","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3385412.3385985","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:41:14Z","timestamp":1750200074000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3385412.3385985"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,6,11]]},"references-count":33,"alternative-id":["10.1145\/3385412.3385985","10.1145\/3385412"],"URL":"https:\/\/doi.org\/10.1145\/3385412.3385985","relation":{},"subject":[],"published":{"date-parts":[[2020,6,11]]},"assertion":[{"value":"2020-06-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}