{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:43:10Z","timestamp":1773193390017,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":46,"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:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"German Research Foundation (DFG)","award":["389792660 (TRR 248)"],"award-info":[{"award-number":["389792660 (TRR 248)"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,11,8]]},"DOI":"10.1145\/3368089.3409763","type":"proceedings-article","created":{"date-parts":[[2020,11,8]],"date-time":"2020-11-08T06:03:47Z","timestamp":1604815427000},"page":"701-712","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":44,"title":["Detecting critical bugs in SMT solvers using blackbox mutational fuzzing"],"prefix":"10.1145","author":[{"given":"Muhammad Numair","family":"Mansur","sequence":"first","affiliation":[{"name":"MPI-SWS, Germany"}]},{"given":"Maria","family":"Christakis","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}]},{"given":"Valentin","family":"W\u00fcstholz","sequence":"additional","affiliation":[{"name":"ConsenSys, Germany"}]},{"given":"Fuyuan","family":"Zhang","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}]}],"member":"320","published-online":{"date-parts":[[2020,11,8]]},"reference":[{"key":"e_1_3_2_2_1_1","unstructured":"[n.d.]. CREST: Concolic Test Generation Tool for C. http:\/\/www.burn.im\/crest\/.  [n.d.]. CREST: Concolic Test Generation Tool for C. http:\/\/www.burn.im\/crest\/."},{"key":"e_1_3_2_2_2_1","unstructured":"[n.d.]. DeltaSMT. http:\/\/fmv.jku.at\/deltasmt.  [n.d.]. DeltaSMT. http:\/\/fmv.jku.at\/deltasmt."},{"key":"e_1_3_2_2_3_1","unstructured":"[n.d.]. The International Satisfiability Modulo Theories Competition. https: \/\/smt-comp.github.io.  [n.d.]. The International Satisfiability Modulo Theories Competition. https: \/\/smt-comp.github.io."},{"key":"e_1_3_2_2_4_1","unstructured":"[n.d.]. The Satisfiability Modulo Theories Library. http:\/\/smtlib.cs.uiowa.edu.  [n.d.]. The Satisfiability Modulo Theories Library. http:\/\/smtlib.cs.uiowa.edu."},{"key":"e_1_3_2_2_5_1","volume-title":"\u201cWhitepaper","author":"Technical","unstructured":"[n.d.]. Technical \u201cWhitepaper \u201d for AFL. http:\/\/lcamtuf.coredump.cx\/afl\/ technical_details.txt. [n.d.]. Technical \u201cWhitepaper\u201d for AFL. http:\/\/lcamtuf.coredump.cx\/afl\/ technical_details.txt."},{"key":"e_1_3_2_2_6_1","unstructured":"[n.d.]. VoteSMT. http:\/\/fmv.jku.at\/votesmt.  [n.d.]. VoteSMT. http:\/\/fmv.jku.at\/votesmt."},{"key":"e_1_3_2_2_7_1","volume-title":"TAP (LNCS","author":"Artho Cyrille","unstructured":"Cyrille Artho , Armin Biere , and Martina Seidl . 2013. Model-Based Testing for Verification Back-Ends . In TAP (LNCS , Vol. 7942 ). Springer , 39-55. Cyrille Artho, Armin Biere, and Martina Seidl. 2013. Model-Based Testing for Verification Back-Ends. In TAP (LNCS, Vol. 7942 ). Springer, 39-55."},{"key":"e_1_3_2_2_8_1","volume-title":"Robert DeLine, Bart Jacobs, and K. Rustan M. Leino.","author":"Barnett Michael","year":"2005","unstructured":"Michael Barnett , Bor-Yuh Evan Chang , Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. 2005 . Boogie : A Modular Reusable Verifier for Object-Oriented Programs. In FMCO (LNCS, Vol. 4111 ). Springer , 364-387. Michael Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. 2005. Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In FMCO (LNCS, Vol. 4111 ). Springer, 364-387."},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"crossref","unstructured":"Earl T. Barr Mark Harman Phil McMinn Muzammil Shahbaz and Shin Yoo. 2015. The Oracle Problem in Software Testing: A Survey. TSE 41 ( 2015 ) 507-525. Issue 5.  Earl T. Barr Mark Harman Phil McMinn Muzammil Shahbaz and Shin Yoo. 2015. The Oracle Problem in Software Testing: A Survey. TSE 41 ( 2015 ) 507-525. Issue 5.","DOI":"10.1109\/TSE.2014.2372785"},{"key":"e_1_3_2_2_10_1","volume-title":"CAV (LNCS","author":"Barrett Clark W.","unstructured":"Clark W. Barrett , Christopher L. Conway , Morgan Deters , Liana Hadarean , Dejan Jovanovic , Tim King , Andrew Reynolds , and Cesare Tinelli . 2011. CVC4 . In CAV (LNCS , Vol. 6806 ). Springer , 171-177. Clark W. Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, and Cesare Tinelli. 2011. CVC4. In CAV (LNCS, Vol. 6806 ). Springer, 171-177."},{"key":"e_1_3_2_2_11_1","volume-title":"Barrett and Cesare Tinelli","author":"Clark","year":"2018","unstructured":"Clark W. Barrett and Cesare Tinelli . 2018 . Satisfiability Modulo Theories. In Handbook of Model Checking. Springer , 305-343. Clark W. Barrett and Cesare Tinelli. 2018. Satisfiability Modulo Theories. In Handbook of Model Checking. Springer, 305-343."},{"key":"e_1_3_2_2_12_1","first-page":"55","article-title":"Z3str3: A String Solver with Theory-Aware Heuristics","author":"Berzish Murphy","year":"2017","unstructured":"Murphy Berzish , Vijay Ganesh , and Yunhui Zheng . 2017 . Z3str3: A String Solver with Theory-Aware Heuristics . In FMCAD. IEEE Computer Society , 55 - 59 . Murphy Berzish, Vijay Ganesh, and Yunhui Zheng. 2017. Z3str3: A String Solver with Theory-Aware Heuristics. In FMCAD. IEEE Computer Society, 55-59.","journal-title":"FMCAD. IEEE Computer Society"},{"key":"e_1_3_2_2_13_1","volume-title":"CAV (LNCS","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 CAV (LNCS , Vol. 10982 ). Springer , 45-51. Dmitry Blotsky, Federico Mora, Murphy Berzish, Yunhui Zheng, Ifaz Kabir, and Vijay Ganesh. 2018. StringFuzz: A Fuzzer for String Solvers. In CAV (LNCS, Vol. 10982 ). Springer, 45-51."},{"key":"e_1_3_2_2_14_1","first-page":"1","article-title":"Fuzzing and Delta-Debugging SMT Solvers","author":"Brummayer Robert","year":"2009","unstructured":"Robert Brummayer and Armin Biere . 2009 . Fuzzing and Delta-Debugging SMT Solvers . In SMT. ACM , 1 - 5 . Robert Brummayer and Armin Biere. 2009. Fuzzing and Delta-Debugging SMT Solvers. In SMT. ACM, 1-5.","journal-title":"SMT. ACM"},{"key":"e_1_3_2_2_15_1","volume-title":"SAT (LNCS","author":"Brummayer Robert","unstructured":"Robert Brummayer , Florian Lonsing , and Armin Biere . 2010. Automated Testing and Debugging of SAT and QBF Solvers . In SAT (LNCS , Vol. 6175 ). Springer , 44-57. Robert Brummayer, Florian Lonsing, and Armin Biere. 2010. Automated Testing and Debugging of SAT and QBF Solvers. In SAT (LNCS, Vol. 6175 ). Springer, 44-57."},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"crossref","unstructured":"Alexandra Bugariu and Peter M\u00fcller. 2020. Automatically Testing String Solvers. In ICSE. To appear.  Alexandra Bugariu and Peter M\u00fcller. 2020. Automatically Testing String Solvers. In ICSE. To appear.","DOI":"10.1145\/3377811.3380398"},{"key":"e_1_3_2_2_17_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. ACM , 768 - 778 . Alexandra Bugariu, Valentin W\u00fcstholz, Maria Christakis, and Peter M\u00fcller. 2018. Automatically Testing Implementations of Numerical Abstract Domains. In ASE. ACM, 768-778.","journal-title":"ASE. ACM"},{"key":"e_1_3_2_2_18_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. USENIX , 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. USENIX, 209-224."},{"key":"e_1_3_2_2_19_1","volume-title":"SPIN (LNCS","author":"Christ J\u00fcrgen","unstructured":"J\u00fcrgen Christ , Jochen Hoenicke , and Alexander Nutz . 2012. SMTInterpol: An Interpolating SMT Solver . In SPIN (LNCS , Vol. 7385 ). Springer , 248-254. J\u00fcrgen Christ, Jochen Hoenicke, and Alexander Nutz. 2012. SMTInterpol: An Interpolating SMT Solver. In SPIN (LNCS, Vol. 7385 ). Springer, 248-254."},{"key":"e_1_3_2_2_20_1","volume-title":"Bastiaan Joost Schaafsma, and Roberto Sebastiani","author":"Cimatti Alessandro","year":"2013","unstructured":"Alessandro Cimatti , Alberto Griggio , Bastiaan Joost Schaafsma, and Roberto Sebastiani . 2013 . The MathSAT5 SMT Solver. In TACAS (LNCS, Vol. 7795 ). Springer , 93-107. Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, and Roberto Sebastiani. 2013. The MathSAT5 SMT Solver. In TACAS (LNCS, Vol. 7795 ). Springer, 93-107."},{"key":"e_1_3_2_2_21_1","unstructured":"Lo\u00efc Correnson Pascal Cuoq Florent Kirchner Virgile Prevosto Armand Puccetti Julien Signoles and Boris Yakobowski. 2011. Frama-C User Manual. http:\/\/framac.com\/\/support.html.  Lo\u00efc Correnson Pascal Cuoq Florent Kirchner Virgile Prevosto Armand Puccetti Julien Signoles and Boris Yakobowski. 2011. Frama-C User Manual. http:\/\/framac.com\/\/support.html."},{"key":"e_1_3_2_2_22_1","first-page":"238","article-title":"Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints","author":"Cousot Patrick","year":"1977","unstructured":"Patrick Cousot and Radhia Cousot . 1977 . Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints . In POPL. ACM , 238 - 252 . Patrick Cousot and Radhia Cousot. 1977. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In POPL. ACM, 238-252.","journal-title":"POPL. ACM"},{"key":"e_1_3_2_2_23_1","volume-title":"NFM (LNCS","author":"Cuoq Pascal","unstructured":"Pascal Cuoq , Benjamin Monate , Anne Pacalet , Virgile Prevosto , John Regehr , Boris Yakobowski , and Xuejun Yang . 2012. Testing Static Analyzers with Randomly Generated Programs . In NFM (LNCS , Vol. 7226 ). Springer , 120-125. Pascal Cuoq, Benjamin Monate, Anne Pacalet, Virgile Prevosto, John Regehr, Boris Yakobowski, and Xuejun Yang. 2012. Testing Static Analyzers with Randomly Generated Programs. In NFM (LNCS, Vol. 7226 ). Springer, 120-125."},{"key":"e_1_3_2_2_24_1","volume-title":"TACAS (LNCS","author":"de Moura Leonardo","unstructured":"Leonardo de Moura and Nikolaj Bj\u00f8rner . 2008. Z3: An Eficient SMT Solver . In TACAS (LNCS , Vol. 4963 ). Springer , 337-340. Leonardo de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Eficient SMT Solver. In TACAS (LNCS, Vol. 4963 ). Springer, 337-340."},{"key":"e_1_3_2_2_25_1","volume-title":"VMCAI (LNCS","author":"de Moura Leonardo","unstructured":"Leonardo de Moura and Dejan Jovanovic . 2013. A Model-Constructing Satisfiability Calculus . In VMCAI (LNCS , Vol. 7737 ). Springer , 1-12. Leonardo de Moura and Dejan Jovanovic. 2013. A Model-Constructing Satisfiability Calculus. In VMCAI (LNCS, Vol. 7737 ). Springer, 1-12."},{"key":"e_1_3_2_2_26_1","volume-title":"CAV (LNCS","author":"Dutertre Bruno","unstructured":"Bruno Dutertre . 2014. Yices 2.2. In CAV (LNCS , Vol. 8559 ). Springer , 737-744. Bruno Dutertre. 2014. Yices 2.2. In CAV (LNCS, Vol. 8559 ). Springer, 737-744."},{"key":"e_1_3_2_2_27_1","volume-title":"CADE (LNCS","author":"Ford Jonathan","unstructured":"Jonathan Ford and Natarajan Shankar . 2002. Formal Verification of a Combination Decision Procedure . In CADE (LNCS , Vol. 2392 ). Springer , 347-362. Jonathan Ford and Natarajan Shankar. 2002. Formal Verification of a Combination Decision Procedure. In CADE (LNCS, Vol. 2392 ). Springer, 347-362."},{"key":"e_1_3_2_2_29_1","volume-title":"Dill","author":"Ganesh Vijay","year":"2007","unstructured":"Vijay Ganesh and David L . Dill . 2007 . A Decision Procedure for Bit-Vectors and Arrays. In CAV (LNCS, Vol. 4590 ). Springer , 519-531. Vijay Ganesh and David L. Dill. 2007. A Decision Procedure for Bit-Vectors and Arrays. In CAV (LNCS, Vol. 4590 ). Springer, 519-531."},{"key":"e_1_3_2_2_30_1","first-page":"151","article-title":"Automated Whitebox Fuzz Testing","author":"Godefroid Patrice","year":"2008","unstructured":"Patrice Godefroid , Michael Y. Levin , and David A. Molnar . 2008 . Automated Whitebox Fuzz Testing . In NDSS. The Internet Society , 151 - 166 . Patrice Godefroid, Michael Y. Levin, and David A. Molnar. 2008. Automated Whitebox Fuzz Testing. In NDSS. The Internet Society, 151-166.","journal-title":"NDSS. The Internet Society"},{"key":"e_1_3_2_2_31_1","first-page":"173","article-title":"The Design and Implementation of the Model-Constructing Satisfiability Calculus","author":"Jovanovic Dejan","year":"2013","unstructured":"Dejan Jovanovic , Clark Barrett , and Leonardo de Moura . 2013 . The Design and Implementation of the Model-Constructing Satisfiability Calculus . In FMCAD. IEEE Computer Society , 173 - 180 . Dejan Jovanovic, Clark Barrett, and Leonardo de Moura. 2013. The Design and Implementation of the Model-Constructing Satisfiability Calculus. In FMCAD. IEEE Computer Society, 173-180.","journal-title":"FMCAD. IEEE Computer Society"},{"key":"e_1_3_2_2_32_1","first-page":"590","article-title":"Automatic Testing of Symbolic Execution Engines via Program Generation and Diferential Testing","author":"Kapus Timotej","year":"2017","unstructured":"Timotej Kapus and Cristian Cadar . 2017 . Automatic Testing of Symbolic Execution Engines via Program Generation and Diferential Testing . In ASE. IEEE Computer Society , 590 - 600 . Timotej Kapus and Cristian Cadar. 2017. Automatic Testing of Symbolic Execution Engines via Program Generation and Diferential Testing. In ASE. IEEE Computer Society, 590-600.","journal-title":"ASE. IEEE Computer Society"},{"key":"e_1_3_2_2_33_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. ACM , 239 - 250 . Christian Klinger, Maria Christakis, and Valentin W\u00fcstholz. 2019. Diferentially Testing Soundness and Precision of Program Analyzers. In ISSTA. ACM, 239-250.","journal-title":"ISSTA. ACM"},{"key":"e_1_3_2_2_34_1","volume-title":"Dafny: An Automatic Program Verifier for Functional Correctness. In LPAR (LNCS","author":"Leino K. Rustan M.","year":"2010","unstructured":"K. Rustan M. Leino . 2010 . Dafny: An Automatic Program Verifier for Functional Correctness. In LPAR (LNCS , Vol. 6355 ). Springer , 348-370. K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In LPAR (LNCS, Vol. 6355 ). Springer, 348-370."},{"key":"e_1_3_2_2_35_1","unstructured":"St\u00e9phane Lescuyer and Sylvain Conchon. 2008. A Reflexive Formalization of a SAT Solver in Coq. In TPHOLs.  St\u00e9phane Lescuyer and Sylvain Conchon. 2008. A Reflexive Formalization of a SAT Solver in Coq. In TPHOLs."},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737965"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"crossref","unstructured":"Filip Maric. 2010. Formal Verification of a Modern SAT Solver by Shallow Embedding into Isabelle\/HOL. TCS 411 ( 2010 ) 4333-4356. Issue 50.  Filip Maric. 2010. Formal Verification of a Modern SAT Solver by Shallow Embedding into Isabelle\/HOL. TCS 411 ( 2010 ) 4333-4356. Issue 50.","DOI":"10.1016\/j.tcs.2010.09.014"},{"key":"e_1_3_2_2_38_1","first-page":"337","article-title":"Path-Exploration Lifting","author":"Martignoni Lorenzo","year":"2012","unstructured":"Lorenzo Martignoni , Stephen McCamant , Pongsin Poosankam , Dawn Song , and Petros Maniatis . 2012 . Path-Exploration Lifting : Hi-Fi Tests for Lo-Fi Emulators. In ASPLOS. ACM , 337 - 348 . Lorenzo Martignoni, Stephen McCamant, Pongsin Poosankam, Dawn Song, and Petros Maniatis. 2012. Path-Exploration Lifting: Hi-Fi Tests for Lo-Fi Emulators. In ASPLOS. ACM, 337-348.","journal-title":"Hi-Fi Tests for Lo-Fi Emulators. In ASPLOS. ACM"},{"key":"e_1_3_2_2_39_1","unstructured":"William M. McKeeman. 1998. Diferential Testing for Software. Digital Technical Journal 10 ( 1998 ) 100-107. Issue 1.  William M. McKeeman. 1998. Diferential Testing for Software. Digital Technical Journal 10 ( 1998 ) 100-107. Issue 1."},{"key":"e_1_3_2_2_40_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_3_2_2_41_1","unstructured":"Aina Niemetz Mathias Preiner and Armin Biere. 2017. Model-Based API Testing for SMT Solvers. In SMT. 10 pages.  Aina Niemetz Mathias Preiner and Armin Biere. 2017. Model-Based API Testing for SMT Solvers. In SMT. 10 pages."},{"key":"e_1_3_2_2_42_1","volume-title":"CAV (LNCS","author":"Niemetz Aina","unstructured":"Aina Niemetz , Mathias Preiner , Cliford Wolf , and Armin Biere . 2018. Btor2, Btor MC and Boolector 3.0. In CAV (LNCS , Vol. 10981 ). Springer , 587-595. Aina Niemetz, Mathias Preiner, Cliford Wolf, and Armin Biere. 2018. Btor2, BtorMC and Boolector 3.0. In CAV (LNCS, Vol. 10981 ). Springer, 587-595."},{"key":"e_1_3_2_2_43_1","first-page":"9","article-title":"Views on Internal and External Validity in Empirical Software Engineering","author":"Siegmund Janet","year":"2015","unstructured":"Janet Siegmund , Norbert Siegmund , and Sven Apel . 2015 . Views on Internal and External Validity in Empirical Software Engineering . In ICSE. IEEE Computer Society , 9 - 19 . Janet Siegmund, Norbert Siegmund, and Sven Apel. 2015. Views on Internal and External Validity in Empirical Software Engineering. In ICSE. IEEE Computer Society, 9-19.","journal-title":"ICSE. IEEE Computer Society"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368826.3377927"},{"key":"e_1_3_2_2_45_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. ACM , 283 - 294 . Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. 2011. Finding and Understanding Bugs in C Compilers. In PLDI. ACM, 283-294.","journal-title":"PLDI. ACM"},{"key":"e_1_3_2_2_46_1","volume-title":"Why Programs Fail","author":"Zeller Andreas","unstructured":"Andreas Zeller . 2009. Why Programs Fail , Second Edition: A Guide to Systematic Debugging. Morgan Kaufmann . Andreas Zeller. 2009. Why Programs Fail, Second Edition: A Guide to Systematic Debugging. Morgan Kaufmann."},{"key":"e_1_3_2_2_47_1","first-page":"763","article-title":"Finding and Understanding Bugs in Software Model Checkers","author":"Zhang Chengyu","year":"2019","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. ACM , 763 - 773 . 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. ACM, 763-773.","journal-title":"ESEC\/FSE. ACM"}],"event":{"name":"ESEC\/FSE '20: 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering","location":"Virtual Event USA","acronym":"ESEC\/FSE '20","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"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.3409763","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3368089.3409763","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:01:58Z","timestamp":1750197718000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3368089.3409763"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,8]]},"references-count":46,"alternative-id":["10.1145\/3368089.3409763","10.1145\/3368089"],"URL":"https:\/\/doi.org\/10.1145\/3368089.3409763","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"}}]}}