{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T04:41:24Z","timestamp":1769748084968,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":53,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,8,12]],"date-time":"2019-08-12T00:00:00Z","timestamp":1565568000000},"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":[[2019,8,12]]},"DOI":"10.1145\/3338906.3338932","type":"proceedings-article","created":{"date-parts":[[2019,8,9]],"date-time":"2019-08-09T12:21:03Z","timestamp":1565353263000},"page":"763-773","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":24,"title":["Finding and understanding bugs in software model checkers"],"prefix":"10.1145","author":[{"given":"Chengyu","family":"Zhang","sequence":"first","affiliation":[{"name":"East China Normal University, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ting","family":"Su","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yichen","family":"Yan","sequence":"additional","affiliation":[{"name":"East China Normal University, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fuyuan","family":"Zhang","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Geguang","family":"Pu","sequence":"additional","affiliation":[{"name":"East China Normal University, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhendong","family":"Su","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,8,12]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"List of bugs found by MCFuzz. Retrieved","author":"Anonymous","year":"2019","unstructured":"Anonymous . 2019. List of bugs found by MCFuzz. Retrieved Feb. 2019 from https:\/\/github.com\/MCFuzzer Anonymous. 2019. List of bugs found by MCFuzz. Retrieved Feb. 2019 from https:\/\/github.com\/MCFuzzer"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503274"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2014.2372785"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54580-5_20"},{"key":"e_1_3_2_1_6_1","unstructured":"Dirk Beyer Adam Chlipala Thomas A. Henzinger Ranjit Jhala and Rupak Majumdar. 2004. Generating Tests from Counterexamples. In ICSE. 326\u2013335.   Dirk Beyer Adam Chlipala Thomas A. Henzinger Ranjit Jhala and Rupak Majumdar. 2004. Generating Tests from Counterexamples. In ICSE. 326\u2013335."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/3220881.3220981"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Dirk Beyer and M Erkan Keremoglu. 2011. CPAchecker: A tool for configurable software verification. In CAV. 184\u2013190.   Dirk Beyer and M Erkan Keremoglu. 2011. CPAchecker: A tool for configurable software verification. In CAV. 184\u2013190.","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"e_1_3_2_1_9_1","volume-title":"Software Verification: Testing vs. Model Checking. In HVC. 99\u2013114.","author":"Beyer Dirk","year":"2017","unstructured":"Dirk Beyer and Thomas Lemberger . 2017 . Software Verification: Testing vs. Model Checking. In HVC. 99\u2013114. Dirk Beyer and Thomas Lemberger. 2017. Software Verification: Testing vs. Model Checking. In HVC. 99\u2013114."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Armin Biere Alessandro Cimatti Edmund Clarke and Yunshan Zhu. 1999. Symbolic model checking without BDDs. In TACAS. 193\u2013207.   Armin Biere Alessandro Cimatti Edmund Clarke and Yunshan Zhu. 1999. Symbolic model checking without BDDs. In TACAS. 193\u2013207.","DOI":"10.1007\/3-540-49059-0_14"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Aaron R. Bradley. 2011. SAT-based model checking without unrolling. In VMCAI. 70\u201387.   Aaron R. Bradley. 2011. SAT-based model checking without unrolling. In VMCAI. 70\u201387.","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_4"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3240464"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2889160.2889206"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_23"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Edmund Clarke Daniel Kroening and Flavio Lerda. 2004. A tool for checking ANSI-C programs. In TACAS. 168\u2013176.  Edmund Clarke Daniel Kroening and Flavio Lerda. 2004. A tool for checking ANSI-C programs. In TACAS. 168\u2013176.","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28891-3_12"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1287624.1287651"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"crossref","unstructured":"Alastair F. Donaldson Leopold Haller Daniel Kroening and Philipp R\u00fcmmer. 2011. Software verification using k-induction. In SAS. 351\u2013368.   Alastair F. Donaldson Leopold Haller Daniel Kroening and Philipp R\u00fcmmer. 2011. Software verification using k-induction. In SAS. 351\u2013368.","DOI":"10.1007\/978-3-642-23702-7_26"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2008.923410"},{"key":"e_1_3_2_1_24_1","volume-title":"Infer static analyzer. Retrieved","year":"2019","unstructured":"Facebook. 2019. Infer static analyzer. Retrieved Feb. 2019 from http:\/\/fbinfer.com\/ Facebook. 2019. Infer static analyzer. Retrieved Feb. 2019 from http:\/\/fbinfer.com\/"},{"key":"e_1_3_2_1_25_1","first-page":"215","article-title":"Testing with model checkers: a survey","volume":"19","author":"Fraser Gordon","year":"2009","unstructured":"Gordon Fraser , Franz Wotawa , and Paul Ammann . 2009 . Testing with model checkers: a survey . STVR 19 , 3 (2009), 215 \u2013 261 . Gordon Fraser, Franz Wotawa, and Paul Ammann. 2009. Testing with model checkers: a survey. STVR 19, 3 (2009), 215\u2013261.","journal-title":"STVR"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"crossref","unstructured":"Susanne Graf and Hassen Sa\u00efdi. 1997. Construction of abstract state graphs with PVS. In CAV. 72\u201383.   Susanne Graf and Hassen Sa\u00efdi. 1997. Construction of abstract state graphs with PVS. In CAV. 72\u201383.","DOI":"10.1007\/3-540-63166-6_10"},{"key":"e_1_3_2_1_27_1","volume-title":"Navas","author":"Gurfinkel Arie","year":"2015","unstructured":"Arie Gurfinkel , Temesghen Kahsai , Anvesh Komuravelli , and Jorge A . Navas . 2015 . The SeaHorn verification framework. In CAV. 343\u2013361. Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, and Jorge A. Navas. 2015. The SeaHorn verification framework. In CAV. 343\u2013361."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/379605.379665"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592438"},{"key":"e_1_3_2_1_30_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.   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_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11486-1_14"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"crossref","unstructured":"Anvesh Komuravelli Arie Gurfinkel Sagar Chaki and Edmund M Clarke. 2013. Automatic abstraction in SMT-based unbounded software model checking. In CAV. 846\u2013862.  Anvesh Komuravelli Arie Gurfinkel Sagar Chaki and Edmund M Clarke. 2013. Automatic abstraction in SMT-based unbounded software model checking. In CAV. 846\u2013862.","DOI":"10.1007\/978-3-642-39799-8_59"},{"key":"e_1_3_2_1_33_1","volume-title":"LLVM: A compilation framework for lifelong program analysis &amp","author":"Lattner Chris","year":"2004","unstructured":"Chris Lattner and Vikram Adve . 2004 . LLVM: A compilation framework for lifelong program analysis &amp ; transformation. In CGO. 75. Chris Lattner and Vikram Adve. 2004. LLVM: A compilation framework for lifelong program analysis & transformation. In CGO. 75."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594334"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814319"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737986"},{"key":"e_1_3_2_1_38_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 \u2013 107 . William M. McKeeman. 1998. Differential Testing for Software. Digital Technical Journal 10, 1 (1998), 100\u2013107.","journal-title":"Digital Technical Journal"},{"key":"e_1_3_2_1_39_1","volume-title":"Quickchecking static analysis properties. STVR 27, 6","author":"Midtgaard Jan","year":"2017","unstructured":"Jan Midtgaard and Anders M\u00f8ller . 2017. Quickchecking static analysis properties. STVR 27, 6 ( 2017 ). Jan Midtgaard and Anders M\u00f8ller. 2017. Quickchecking static analysis properties. STVR 27, 6 (2017)."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236029"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2970276.2970305"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3213846.3213873"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984038"},{"key":"e_1_3_2_1_44_1","volume-title":"Competition on Software Verification (SV-COMP). Retrieved","author":"SV-COMP.","year":"2019","unstructured":"SV-COMP. 2019. Competition on Software Verification (SV-COMP). Retrieved Feb. 2019 from https:\/\/sv-comp.sosy-lab.org\/2019\/ SV-COMP. 2019. Competition on Software Verification (SV-COMP). Retrieved Feb. 2019 from https:\/\/sv-comp.sosy-lab.org\/2019\/"},{"key":"e_1_3_2_1_45_1","volume-title":"Clang 9 documentation: LibTooling. Retrieved","author":"Team The Clang","year":"2019","unstructured":"The Clang Team . 2019. Clang 9 documentation: LibTooling. Retrieved Feb. 2019 from https:\/\/clang.llvm.org\/docs\/LibTooling.html The Clang Team. 2019. Clang 9 documentation: LibTooling. Retrieved Feb. 2019 from https:\/\/clang.llvm.org\/docs\/LibTooling.html"},{"key":"e_1_3_2_1_46_1","volume-title":"Using the CompCert C interpreter. Retrieved","author":"CompCert Team The","year":"2019","unstructured":"The CompCert Team . 2019. Using the CompCert C interpreter. Retrieved Feb. 2019 from http:\/\/compcert.inria.fr\/man\/manual004.html The CompCert Team. 2019. Using the CompCert C interpreter. Retrieved Feb. 2019 from http:\/\/compcert.inria.fr\/man\/manual004.html"},{"key":"e_1_3_2_1_47_1","unstructured":"The Eclipse Team. 2019. Eclipse CDT (C\/C++ Development Tooling). Retrieved Feb. 2019 from https:\/\/www.eclipse.org\/cdt\/  The Eclipse Team. 2019. Eclipse CDT (C\/C++ Development Tooling). Retrieved Feb. 2019 from https:\/\/www.eclipse.org\/cdt\/"},{"key":"e_1_3_2_1_48_1","volume-title":"the GNU Compiler Collection. Retrieved","author":"Team The GCC","year":"2019","unstructured":"The GCC Team . 2019. GCC , the GNU Compiler Collection. Retrieved Feb. 2019 from https:\/\/gcc.gnu.org\/ The GCC Team. 2019. GCC, the GNU Compiler Collection. Retrieved Feb. 2019 from https:\/\/gcc.gnu.org\/"},{"key":"e_1_3_2_1_49_1","unstructured":"The ISO Team. 2019. ISO\/IEC 9899:2018:Information technology \u2013 Programming languages \u2013 C. Retrieved Feb. 2019 from https:\/\/www.iso.org\/standard\/74528.  The ISO Team. 2019. ISO\/IEC 9899:2018:Information technology \u2013 Programming languages \u2013 C. Retrieved Feb. 2019 from https:\/\/www.iso.org\/standard\/74528."},{"key":"e_1_3_2_1_50_1","unstructured":"html  html"},{"key":"e_1_3_2_1_51_1","volume-title":"7th Competition on Software Verification (SVCOMP). Retrieved","author":"Team The SVCOMP","year":"2019","unstructured":"The SVCOMP Team . 2019. 7th Competition on Software Verification (SVCOMP). Retrieved Feb. 2019 from https:\/\/sv-comp.sosy-lab.org\/2018\/results\/ results-verified\/ The SVCOMP Team. 2019. 7th Competition on Software Verification (SVCOMP). Retrieved Feb. 2019 from https:\/\/sv-comp.sosy-lab.org\/2018\/results\/ results-verified\/"},{"key":"e_1_3_2_1_52_1","volume-title":"SMTInterpol: an Interpolating SMT Solver. Retrieved","author":"Interpol Team The","year":"2019","unstructured":"The SMT Interpol Team . 2019. SMTInterpol: an Interpolating SMT Solver. Retrieved Feb. 2019 from https:\/\/ultimate.informatik.uni-freiburg.de\/smtinterpol\/ The SMTInterpol Team. 2019. SMTInterpol: an Interpolating SMT Solver. Retrieved Feb. 2019 from https:\/\/ultimate.informatik.uni-freiburg.de\/smtinterpol\/"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491439"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"}],"event":{"name":"ESEC\/FSE '19: 27th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering","location":"Tallinn Estonia","acronym":"ESEC\/FSE '19","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 2019 27th 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\/3338906.3338932","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3338906.3338932","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:26:20Z","timestamp":1750206380000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3338906.3338932"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,8,12]]},"references-count":53,"alternative-id":["10.1145\/3338906.3338932","10.1145\/3338906"],"URL":"https:\/\/doi.org\/10.1145\/3338906.3338932","relation":{},"subject":[],"published":{"date-parts":[[2019,8,12]]},"assertion":[{"value":"2019-08-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}