{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T13:33:29Z","timestamp":1790948009611,"version":"4.1.0"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2020,11,13]],"date-time":"2020-11-13T00:00:00Z","timestamp":1605225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,11,13]]},"abstract":"<jats:p>We propose type-aware operator mutation, a simple, but unusually effective approach for testing SMT solvers. The key idea is to mutate operators of conforming types within the seed formulas to generate well-typed mutant formulas. These mutant formulas are then used as the test cases for SMT solvers. We realized type-aware operator mutation within the OpFuzz tool and used it to stress-test Z3 and CVC4, two state-of-the-art SMT solvers. Type-aware operator mutations are unusually effective: During one year of extensive testing with OpFuzz, we reported 1092 bugs on Z3\u2019s and CVC4\u2019s respective GitHub issue trackers, out of which 819 unique bugs were confirmed and 685 of the confirmed bugs were fixed by the developers. The detected bugs are highly diverse \u2014 we found bugs of many different types (soundness bugs, invalid model bugs, crashes, etc.), logics and solver configurations. We have further conducted an in-depth study of the bugs found by OpFuzz. The study results show that the bugs found by OpFuzz are of high quality. Many of them affect core components of the SMT solvers\u2019 codebases, and some required major changes for the developers to fix. Among the 819 confirmed bugs found by OpFuzz,184 were soundness bugs, the most critical bugs in SMT solvers,and 489 were in the default modes of the solvers. Notably, OpFuzz found 27 critical soundness bugs in CVC4, which has proved to be a very stable SMT solver.<\/jats:p>","DOI":"10.1145\/3428261","type":"journal-article","created":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T23:36:06Z","timestamp":1606260966000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":53,"title":["On the unusual effectiveness of type-aware operator mutations for testing SMT solvers"],"prefix":"10.1145","volume":"4","author":[{"given":"Dominik","family":"Winterer","sequence":"first","affiliation":[{"name":"ETH Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Chengyu","family":"Zhang","sequence":"additional","affiliation":[{"name":"East China Normal University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhendong","family":"Su","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2020,11,13]]},"reference":[{"key":"e_1_2_2_1_1","first-page":"1","article-title":"Fuzzing and delta-debugging SMT solvers","author":"Brummayer Robert","year":"2009","unstructured":"Robert Brummayer and Armin Biere . 2009 b. Fuzzing and delta-debugging SMT solvers . In SMT. 1 - 5 . Robert Brummayer and Armin Biere. 2009b. Fuzzing and delta-debugging SMT solvers. In SMT. 1-5.","journal-title":"SMT."},{"key":"e_1_2_2_2_1","first-page":"459","article-title":"Automatically testing string solvers","author":"Bugariu Alexandra","year":"2020","unstructured":"Alexandra Bugariu and Peter M\u00fcller . 2020 . Automatically testing string solvers . In ICSE. 459 - 1470 . Alexandra Bugariu and Peter M\u00fcller. 2020. Automatically testing string solvers. In ICSE. 459-1470.","journal-title":"ICSE."},{"key":"e_1_2_2_3_1","first-page":"768","article-title":"Automatically testing implementations of numerical abstract domains","author":"Bugariu Alexandra","year":"2018","unstructured":"Alexandra Bugariu , Valentin W\u00fcstholz , Maria Christakis , and Peter M\u00fcller . 2018 . Automatically testing implementations of numerical abstract domains . In ASE. 768 - 778 . Alexandra Bugariu, Valentin W\u00fcstholz, Maria Christakis, and Peter M\u00fcller. 2018. Automatically testing implementations of numerical abstract domains. In ASE. 768-778.","journal-title":"ASE."},{"key":"e_1_2_2_4_1","first-page":"765","article-title":"Analysing the program analyser","author":"Cadar Cristian","year":"2016","unstructured":"Cristian Cadar and Alastair Donaldson . 2016 . Analysing the program analyser . In ICSE. 765 - 768 . Cristian Cadar and Alastair Donaldson. 2016. Analysing the program analyser. In ICSE. 765-768.","journal-title":"ICSE."},{"key":"e_1_2_2_5_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-224. 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-224."},{"key":"e_1_2_2_6_1","first-page":"725","article-title":"Program-adaptive mutational fuzzing","author":"Cha Sang Kil","year":"2015","unstructured":"Sang Kil Cha , Maverick Woo , and David Brumley . 2015 . Program-adaptive mutational fuzzing . In SP. 725 - 741 . Sang Kil Cha, Maverick Woo, and David Brumley. 2015. Program-adaptive mutational fuzzing. In SP. 725-741.","journal-title":"SP."},{"key":"e_1_2_2_7_1","first-page":"93","article-title":"The MathSAT5 SMT solver","author":"Cimatti Alessandro","year":"2013","unstructured":"Alessandro Cimatti , Alberto Griggio , Bastiaan Schaafsma , and Roberto Sebastiani . 2013 . The MathSAT5 SMT solver . In TACAS. 93 - 107 . Alessandro Cimatti, Alberto Griggio, Bastiaan Schaafsma, and Roberto Sebastiani. 2013. The MathSAT5 SMT solver. In TACAS. 93-107.","journal-title":"TACAS."},{"key":"e_1_2_2_8_1","unstructured":"The International SMT Competition. 2020. SMT-COMP. Retrieved 2020-05-15 from https:\/\/smt-comp.github.io\/2019\/index. html  The International SMT Competition. 2020. SMT-COMP. Retrieved 2020-05-15 from https:\/\/smt-comp.github.io\/2019\/index. html"},{"key":"e_1_2_2_9_1","first-page":"2123","article-title":"Difuze: Interface aware fuzzing for kernel drivers","author":"Corina Jake","year":"2017","unstructured":"Jake Corina , Aravind Machiry , Christopher Salls , Yan Shoshitaishvili , Shuang Hao , Christopher Kruegel , and Giovanni Vigna . 2017 . Difuze: Interface aware fuzzing for kernel drivers . In CCS. 2123 - 2138 . Jake Corina, Aravind Machiry, Christopher Salls, Yan Shoshitaishvili, Shuang Hao, Christopher Kruegel, and Giovanni Vigna. 2017. Difuze: Interface aware fuzzing for kernel drivers. In CCS. 2123-2138.","journal-title":"CCS."},{"key":"e_1_2_2_10_1","first-page":"95","article-title":"Compiler fuzzing through deep learning","author":"Cummins Chris","year":"2018","unstructured":"Chris Cummins , Pavlos Petoumenos , Alastair Murray , and Hugh Leather . 2018 . Compiler fuzzing through deep learning . In ISSTA. 95 - 105 . Chris Cummins, Pavlos Petoumenos, Alastair Murray, and Hugh Leather. 2018. Compiler fuzzing through deep learning. In ISSTA. 95-105.","journal-title":"ISSTA."},{"key":"e_1_2_2_11_1","first-page":"337","article-title":"CVC4 Regression Test Suite. Retrieved 2020-05-15 from https:\/\/github.com\/CVC4\/CVC4\/tree\/master\/test\/regress Leonardo de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An eficient SMT solver","year":"2020","unstructured":"CVC4. 2020 . CVC4 Regression Test Suite. Retrieved 2020-05-15 from https:\/\/github.com\/CVC4\/CVC4\/tree\/master\/test\/regress Leonardo de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An eficient SMT solver . In TACAS. 337 - 340 . CVC4. 2020. CVC4 Regression Test Suite. Retrieved 2020-05-15 from https:\/\/github.com\/CVC4\/CVC4\/tree\/master\/test\/regress Leonardo de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An eficient SMT solver. In TACAS. 337-340.","journal-title":"TACAS."},{"key":"e_1_2_2_13_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-473. David Detlefs, Greg Nelson, and James B. Saxe. 2005. Simplify: A theorem prover for program checking. JACM ( 2005 ), 365-473."},{"key":"e_1_2_2_14_1","first-page":"213","article-title":"DART: Directed automated random testing","author":"Godefroid Patrice","year":"2005","unstructured":"Patrice Godefroid , Nils Klarlund , and Koushik Sen . 2005 . DART: Directed automated random testing . In PLDI. 213 - 223 . Patrice Godefroid, Nils Klarlund, and Koushik Sen. 2005. DART: Directed automated random testing. In PLDI. 213-223.","journal-title":"PLDI."},{"key":"e_1_2_2_15_1","first-page":"2345","article-title":"Imf: Inferred model-based fuzzer","author":"Han HyungSeok","year":"2017","unstructured":"HyungSeok Han and Sang Kil Cha . 2017 . Imf: Inferred model-based fuzzer . In CCS. 2345 - 2358 . HyungSeok Han and Sang Kil Cha. 2017. Imf: Inferred model-based fuzzer. In CCS. 2345-2358.","journal-title":"CCS."},{"key":"e_1_2_2_16_1","first-page":"57","article-title":"APOLLO: Automatic detection and diagnosis of performance regressions in database systems","author":"Jung Jinho","year":"2019","unstructured":"Jinho Jung , Hong Hu , Joy Arulraj , Taesoo Kim , and Woonhak Kang . 2019 . APOLLO: Automatic detection and diagnosis of performance regressions in database systems . In VLDB. 57 - 70 . Jinho Jung, Hong Hu, Joy Arulraj, Taesoo Kim, and Woonhak Kang. 2019. APOLLO: Automatic detection and diagnosis of performance regressions in database systems. In VLDB. 57-70.","journal-title":"VLDB."},{"key":"e_1_2_2_17_1","first-page":"239","article-title":"Diferentially testing soundness and precision of program analyzers","author":"Klinger Christian","year":"2019","unstructured":"Christian Klinger , Maria Christakis , and Valentin W\u00fcstholz . 2019 . Diferentially testing soundness and precision of program analyzers . In ISSTA. 239 - 250 . Christian Klinger, Maria Christakis, and Valentin W\u00fcstholz. 2019. Diferentially testing soundness and precision of program analyzers. In ISSTA. 239-250.","journal-title":"ISSTA."},{"key":"e_1_2_2_18_1","first-page":"1","article-title":"Coverage guided, property based testing","volume":"181","author":"Lampropoulos Leonidas","year":"2019","unstructured":"Leonidas Lampropoulos , Michael Hicks , and Benjamin C. Pierce . 2019 . Coverage guided, property based testing . In OOPSLA. 181 : 1 - 181 : 29. Leonidas Lampropoulos, Michael Hicks, and Benjamin C. Pierce. 2019. Coverage guided, property based testing. In OOPSLA. 181 : 1-181 : 29.","journal-title":"OOPSLA."},{"key":"e_1_2_2_19_1","first-page":"216","article-title":"Compiler validation via equivalence modulo inputs","author":"Le Vu","year":"2014","unstructured":"Vu Le , Mehrdad Afshari , and Zhendong Su . 2014 . Compiler validation via equivalence modulo inputs . In PLDI. 216 - 226 . Vu Le, Mehrdad Afshari, and Zhendong Su. 2014. Compiler validation via equivalence modulo inputs. In PLDI. 216-226.","journal-title":"PLDI."},{"key":"e_1_2_2_20_1","volume-title":"Fairfuzz: A targeted mutation strategy for increasing greybox fuzz testing coverage. In ASE.","author":"Lemieux Caroline","year":"2018","unstructured":"Caroline Lemieux and Koushik Sen . 2018 . Fairfuzz: A targeted mutation strategy for increasing greybox fuzz testing coverage. In ASE. Caroline Lemieux and Koushik Sen. 2018. Fairfuzz: A targeted mutation strategy for increasing greybox fuzz testing coverage. In ASE."},{"key":"e_1_2_2_21_1","volume-title":"Steelix: Program-state based binary fuzzing. In ESEC\/FSE.","author":"Li Yuekang","year":"2017","unstructured":"Yuekang Li , Bihuan Chen , Mahinthan Chandramohan , Shang-Wei Lin , Yang Liu , and Alwen Tiu . 2017 . Steelix: Program-state based binary fuzzing. In ESEC\/FSE. Yuekang Li, Bihuan Chen, Mahinthan Chandramohan, Shang-Wei Lin, Yang Liu, and Alwen Tiu. 2017. Steelix: Program-state based binary fuzzing. In ESEC\/FSE."},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737986"},{"key":"e_1_2_2_23_1","first-page":"499","article-title":"Generating targeted queries for database testing","author":"Mishra Chaitanya","year":"2008","unstructured":"Chaitanya Mishra , Nick Koudas , and Calisto Zuzarte . 2008 . Generating targeted queries for database testing . In SIGMOD. 499 - 510 . Chaitanya Mishra, Nick Koudas, and Calisto Zuzarte. 2008. Generating targeted queries for database testing. In SIGMOD. 499-510.","journal-title":"SIGMOD."},{"key":"e_1_2_2_24_1","first-page":"36","article-title":"ddSMT: A delta debugger for the SMT-LIB v2 format","author":"Niemetz Aina","year":"2013","unstructured":"Aina Niemetz and Armin Biere . 2013 . ddSMT: A delta debugger for the SMT-LIB v2 format . In SMT. 36 - 45 . Aina Niemetz and Armin Biere. 2013. ddSMT: A delta debugger for the SMT-LIB v2 format. In SMT. 36-45.","journal-title":"SMT."},{"key":"e_1_2_2_25_1","unstructured":"Aina Niemetz Mathias Preiner and Armin Biere. 2017. Model-based API testing for SMT solvers. In SMT. 10.  Aina Niemetz Mathias Preiner and Armin Biere. 2017. Model-based API testing for SMT solvers. In SMT. 10."},{"key":"e_1_2_2_26_1","volume-title":"Detecting critical bugs in SMT solvers using blackbox mutational fuzzing. arXiv e-prints (","author":"Numair Mansur","year":"2020","unstructured":"Mansur Numair , Maria Christakis , Valentin W\u00fcstholz , and Fuyuan Zhang . 2020. Detecting critical bugs in SMT solvers using blackbox mutational fuzzing. arXiv e-prints ( April 2020 ), arXiv: 2004.05934. Mansur Numair, Maria Christakis, Valentin W\u00fcstholz, and Fuyuan Zhang. 2020. Detecting critical bugs in SMT solvers using blackbox mutational fuzzing. arXiv e-prints ( April 2020 ), arXiv: 2004.05934."},{"key":"e_1_2_2_27_1","first-page":"331","article-title":"Do Android taint analysis tools keep their promises?","author":"Pauck Felix","year":"2018","unstructured":"Felix Pauck , Eric Bodden , and Heike Wehrheim . 2018 . Do Android taint analysis tools keep their promises? . In ESEC\/FSE. 331 - 341 . Felix Pauck, Eric Bodden, and Heike Wehrheim. 2018. Do Android taint analysis tools keep their promises?. In ESEC\/FSE. 331-341.","journal-title":"ESEC\/FSE."},{"key":"e_1_2_2_28_1","volume-title":"Alexandru Razvan Caciulescu, and Abhik Roychoudhury.","author":"Pham Van-Thuan","year":"2019","unstructured":"Van-Thuan Pham , Marcel B\u00f6hme , Andrew Edward Santosa , Alexandru Razvan Caciulescu, and Abhik Roychoudhury. 2019 . Smart greybox fuzzing. TSE ( 2019 ). Van-Thuan Pham, Marcel B\u00f6hme, Andrew Edward Santosa, Alexandru Razvan Caciulescu, and Abhik Roychoudhury. 2019. Smart greybox fuzzing. TSE ( 2019 )."},{"key":"e_1_2_2_29_1","first-page":"176","article-title":"Analyzing the analyzers: FlowDroid\/IccTA, AmanDroid, and DroidSafe","author":"Qiu Lina","year":"2018","unstructured":"Lina Qiu , Yingying Wang , and Julia Rubin . 2018 . Analyzing the analyzers: FlowDroid\/IccTA, AmanDroid, and DroidSafe . In ISSTA. 176 - 186 . Lina Qiu, Yingying Wang, and Julia Rubin. 2018. Analyzing the analyzers: FlowDroid\/IccTA, AmanDroid, and DroidSafe. In ISSTA. 176-186.","journal-title":"ISSTA."},{"key":"e_1_2_2_30_1","first-page":"335","article-title":"Test-case reduction for C compiler bugs","author":"Regehr John","year":"2012","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 - 346 . John Regehr, Yang Chen, Pascal Cuoq, Eric Eide, Chucky Ellison, and Xuejun Yang. 2012. Test-case reduction for C compiler bugs. In PLDI. 335-346.","journal-title":"PLDI."},{"key":"e_1_2_2_31_1","doi-asserted-by":"crossref","unstructured":"Andrew Reynolds Morgan Deters Viktor Kuncak Clark W. Barrett and Cesare Tinelli. 2015. On counterexample guided quantifier instantiation for synthesis in CVC4. In CAV.  Andrew Reynolds Morgan Deters Viktor Kuncak Clark W. Barrett and Cesare Tinelli. 2015. On counterexample guided quantifier instantiation for synthesis in CVC4. In CAV.","DOI":"10.1007\/978-3-319-21668-3_12"},{"key":"e_1_2_2_32_1","doi-asserted-by":"crossref","unstructured":"Manuel Rigger and Zhendong Su. 2020. Detecting optimization bugs in database engines via non-optimizing reference Engine Construction. In OOPSLA.  Manuel Rigger and Zhendong Su. 2020. Detecting optimization bugs in database engines via non-optimizing reference Engine Construction. In OOPSLA.","DOI":"10.1145\/3368089.3409710"},{"key":"e_1_2_2_33_1","first-page":"167","article-title":"kAFL: Hardwareassisted feedback fuzzing for OS kernels","author":"Schumilo Sergej","year":"2017","unstructured":"Sergej Schumilo , Cornelius Aschermann , Robert Gawlik , Sebastian Schinzel , and Thorsten Holz . 2017 . kAFL: Hardwareassisted feedback fuzzing for OS kernels . In USENIX Security. 167 - 182 . Sergej Schumilo, Cornelius Aschermann, Robert Gawlik, Sebastian Schinzel, and Thorsten Holz. 2017. kAFL: Hardwareassisted feedback fuzzing for OS kernels. In USENIX Security. 167-182.","journal-title":"USENIX Security."},{"key":"e_1_2_2_34_1","doi-asserted-by":"crossref","unstructured":"Joseph Scott Federico Mora and Vijay Ganesh. 2020. BanditFuzz: Fuzzing SMT solvers with reinforcement learning. In CAV.  Joseph Scott Federico Mora and Vijay Ganesh. 2020. BanditFuzz: Fuzzing SMT solvers with reinforcement learning. In CAV.","DOI":"10.1007\/978-3-030-90870-6_6"},{"key":"e_1_2_2_35_1","volume-title":"Retrieved 2020-08-13 from https:\/\/github.com\/anse1\/sqlsmith SMT-LIB","author":"Seltenreich Andreas","year":"2020","unstructured":"Andreas Seltenreich . 2020. SQLSmith. Retrieved 2020-08-13 from https:\/\/github.com\/anse1\/sqlsmith SMT-LIB . 2020 . SMT-LIB Benchmarks. Retrieved 2020-05-15 from http:\/\/smtlib.cs.uiowa.edu\/benchmarks.shtml Armando Solar-Lezama. 2008. Program synthesis by sketching. Ph.D. Dissertation. UC Berkeley . https:\/\/people.csail.mit. edu\/asolar\/papers\/thesis.pdf Andreas Seltenreich. 2020. SQLSmith. Retrieved 2020-08-13 from https:\/\/github.com\/anse1\/sqlsmith SMT-LIB. 2020. SMT-LIB Benchmarks. Retrieved 2020-05-15 from http:\/\/smtlib.cs.uiowa.edu\/benchmarks.shtml Armando Solar-Lezama. 2008. Program synthesis by sketching. Ph.D. Dissertation. UC Berkeley. https:\/\/people.csail.mit. edu\/asolar\/papers\/thesis.pdf"},{"key":"e_1_2_2_36_1","first-page":"530","article-title":"A lightweight symbolic virtual machine for solver-aided host languages","author":"Torlak Emina","year":"2014","unstructured":"Emina Torlak and Rastislav Bodik . 2014 . A lightweight symbolic virtual machine for solver-aided host languages . In PLDI. 530 - 541 . Emina Torlak and Rastislav Bodik. 2014. A lightweight symbolic virtual machine for solver-aided host languages. In PLDI. 530-541.","journal-title":"PLDI."},{"key":"e_1_2_2_37_1","first-page":"724","article-title":"Superion: Grammar-aware greybox fuzzing","author":"Wang Junjie","year":"2019","unstructured":"Junjie Wang , Bihuan Chen , Lei Wei , and Yang Liu . 2019 . Superion: Grammar-aware greybox fuzzing . In ICSE. 724 - 735 . Junjie Wang, Bihuan Chen, Lei Wei, and Yang Liu. 2019. Superion: Grammar-aware greybox fuzzing. In ICSE. 724-735.","journal-title":"ICSE."},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385985"},{"key":"e_1_2_2_39_1","first-page":"279","article-title":"Efective dynamic detection of alias analysis errors","author":"Wu Jingyue","year":"2013","unstructured":"Jingyue Wu , Gang Hu , Yang Tang , and Junfeng Yang . 2013 . Efective dynamic detection of alias analysis errors . In ESEC\/FSE. 279 - 289 . Jingyue Wu, Gang Hu, Yang Tang, and Junfeng Yang. 2013. Efective dynamic detection of alias analysis errors. In ESEC\/FSE. 279-289.","journal-title":"ESEC\/FSE."},{"key":"e_1_2_2_40_1","first-page":"283","article-title":"Finding and understanding bugs in C compilers","author":"Yang Xuejun","year":"2011","unstructured":"Xuejun Yang , Yang Chen , Eric Eide , and John Regehr . 2011 . Finding and understanding bugs in C compilers . In PLDI. 283 - 294 . Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. 2011. Finding and understanding bugs in C compilers. In PLDI. 283-294.","journal-title":"PLDI."},{"key":"e_1_2_2_41_1","volume-title":"Z3 Regression Test Suite. Retrieved 2020-05-15 from https:\/\/github.com\/Z3Prover\/z3test Michal Zalewski","year":"2020","unstructured":"Z3. 2020. Z3 Regression Test Suite. Retrieved 2020-05-15 from https:\/\/github.com\/Z3Prover\/z3test Michal Zalewski . 2020 . american fuzzy lop. Retrieved 2020-08-12 from https:\/\/lcamtuf.coredump.cx\/afl\/ 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-773. Z3. 2020. Z3 Regression Test Suite. Retrieved 2020-05-15 from https:\/\/github.com\/Z3Prover\/z3test Michal Zalewski. 2020. american fuzzy lop. Retrieved 2020-08-12 from https:\/\/lcamtuf.coredump.cx\/afl\/ 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-773."},{"key":"e_1_2_2_42_1","first-page":"347","article-title":"Skeletal program enumeration for rigorous compiler testing","author":"Zhang Qirun","year":"2017","unstructured":"Qirun Zhang , Chengnian Sun , and Zhendong Su . 2017 . Skeletal program enumeration for rigorous compiler testing . In PLDI. 347 - 361 . Qirun Zhang, Chengnian Sun, and Zhendong Su. 2017. Skeletal program enumeration for rigorous compiler testing. In PLDI. 347-361.","journal-title":"PLDI."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428261","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3428261","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:57Z","timestamp":1750197777000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428261"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,13]]},"references-count":41,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2020,11,13]]}},"alternative-id":["10.1145\/3428261"],"URL":"https:\/\/doi.org\/10.1145\/3428261","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,11,13]]},"assertion":[{"value":"2020-11-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}