{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T20:55:11Z","timestamp":1777582511617,"version":"3.51.4"},"publisher-location":"Cham","reference-count":64,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031572555","type":"print"},{"value":"9783031572562","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T00:00:00Z","timestamp":1712275200000},"content-version":"vor","delay-in-days":95,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Formal verification is essential but challenging: Even the best verifiers may produce wrong verification verdicts.<jats:italic>Certifying<\/jats:italic>verifiers enhance the confidence in verification results by generating a<jats:italic>witness<\/jats:italic>for other tools to validate the verdict independently. Recently, translating the hardware-modeling language<jats:sc>Btor2<\/jats:sc>to software, such as the programming language\u00a0C or LLVM intermediate representation, has been actively studied and facilitated verifying hardware designs by software analyzers. However, it remained unknown whether witnesses produced by software verifiers contain helpful information about the original circuits and how such information can aid hardware analysis. We propose a certifying and validating framework<jats:sc>Btor2<\/jats:sc>-<jats:sc>Cert<\/jats:sc>to verify safety properties of<jats:sc>Btor2<\/jats:sc>circuits, combining<jats:sc>Btor2<\/jats:sc>-to-C translation, software verifiers, and a new witness validator<jats:sc>Btor2<\/jats:sc>-<jats:sc>Val<\/jats:sc>, to answer the above open questions.<jats:sc>Btor2<\/jats:sc>-<jats:sc>Cert<\/jats:sc>translates a software<jats:italic>violation witness<\/jats:italic>to a<jats:sc>Btor2<\/jats:sc>violation witness; As the<jats:sc>Btor2<\/jats:sc>language lacks a format for<jats:italic>correctness witnesses<\/jats:italic>, we encode invariants in software correctness witnesses as<jats:sc>Btor2<\/jats:sc>circuits. The validator<jats:sc>Btor2<\/jats:sc>-<jats:sc>Val<\/jats:sc>checks violation witnesses by circuit simulation and correctness witnesses by<jats:italic>validation via verification<\/jats:italic>. In our evaluation,<jats:sc>Btor2<\/jats:sc>-<jats:sc>Cert<\/jats:sc>successfully utilized software witnesses to improve quality assurance of hardware. By invoking the software verifier<jats:sc>Cbmc<\/jats:sc>on translated programs, it uniquely solved, with confirmed witnesses, 8\u00a0% of the unsafe tasks for which the hardware verifier<jats:sc>ABC<\/jats:sc>failed to detect bugs.<\/jats:p>","DOI":"10.1007\/978-3-031-57256-2_7","type":"book-chapter","created":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T08:03:04Z","timestamp":1712217784000},"page":"129-149","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Btor2-Cert: A Certifying Hardware-Verification Framework Using Software Analyzers"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2354-1750","authenticated-orcid":false,"given":"Zs\u00f3fia","family":"\u00c1d\u00e1m","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4832-7662","authenticated-orcid":false,"given":"Dirk","family":"Beyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5139-5178","authenticated-orcid":false,"given":"Po-Chun","family":"Chien","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8096-5595","authenticated-orcid":false,"given":"Nian-Ze","family":"Lee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-7805-5931","authenticated-orcid":false,"given":"Nils","family":"Sirrenberg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,4,5]]},"reference":[{"key":"7_CR1","doi-asserted-by":"publisher","unstructured":"McConnell, R.M., Mehlhorn, K., N\u00e4her, S., Schweitzer, P.: Certifying algorithms. Computer Science Review 5(2), 119\u2013161 (2011). https:\/\/doi.org\/10.1016\/j.cosrev.2010.09.009","DOI":"10.1016\/j.cosrev.2010.09.009"},{"key":"7_CR2","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M., Lemberger, T., Tautschnig, M.: Verification witnesses. ACM Trans. Softw. Eng. Methodol. 31(4), 57:1\u201357:69 (2022). https:\/\/doi.org\/10.1145\/3477579","DOI":"10.1145\/3477579"},{"key":"7_CR3","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M., Stahlbauer, A.: Witness validation and stepwise testification across software verifiers. In: Proc. FSE. pp. 721\u2013733. ACM (2015). https:\/\/doi.org\/10.1145\/2786805.2786867","DOI":"10.1145\/2786805.2786867"},{"key":"7_CR4","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M.: Correctness witnesses: Exchanging verification results between verifiers. In: Proc. FSE. pp. 326\u2013337. ACM (2016). https:\/\/doi.org\/10.1145\/2950290.2950351","DOI":"10.1145\/2950290.2950351"},{"key":"7_CR5","doi-asserted-by":"publisher","unstructured":"Beyer, D., Chien, P.C., Lee, N.Z.: Bridging hardware and software analysis with Btor2C: A word-level-circuit-to-C translator. In: Proc. TACAS. pp. 1\u201321. LNCS\u00a013994, Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_12","DOI":"10.1007\/978-3-031-30820-8_12"},{"key":"7_CR6","doi-asserted-by":"publisher","unstructured":"Tafese, J., Garcia-Contreras, I., Gurfinkel, A.: Btor2MLIR: A format and toolchain for hardware verification. In: Proc. FMCAD. pp. 55\u201363. IEEE (2023). https:\/\/doi.org\/10.34727\/2023\/ISBN.978-3-85448-060-0_13","DOI":"10.34727\/2023\/ISBN.978-3-85448-060-0_13"},{"key":"7_CR7","doi-asserted-by":"publisher","unstructured":"Niemetz, A., Preiner, M., Wolf, C., Biere, A.: Btor2, BtorMC, and Boolector 3.0. In: Proc. CAV. pp. 587\u2013595. LNCS\u00a010981, Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_32","DOI":"10.1007\/978-3-319-96145-3_32"},{"key":"7_CR8","doi-asserted-by":"publisher","unstructured":"Biere, A., van Dijk, T., Heljanko, K.: Hardware model checking competition 2017. In: Proc. FMCAD. p.\u00a09. IEEE (2017). https:\/\/doi.org\/10.23919\/FMCAD.2017.8102233","DOI":"10.23919\/FMCAD.2017.8102233"},{"key":"7_CR9","unstructured":"Biere, A., Froleyks, N., Preiner, M.: 11th Hardware Model Checking Competition (HWMCC 2020). http:\/\/fmv.jku.at\/hwmcc20\/, accessed: 2023-01-29"},{"key":"7_CR10","unstructured":"ISO\/IEC JTC\u00a01\/SC\u00a022: ISO\/IEC 9899-2018: Information technology \u2014 Programming Languages \u2014 C. International Organization for Standardization (2018), https:\/\/www.iso.org\/standard\/74528.html"},{"key":"7_CR11","doi-asserted-by":"publisher","unstructured":"Lattner, C., Adve, V.S.: LLVM: A compilation framework for lifelong program analysis & transformation. In: Proc. CGO. pp. 75\u201388. IEEE (2004). https:\/\/doi.org\/10.1109\/CGO.2004.1281665","DOI":"10.1109\/CGO.2004.1281665"},{"key":"7_CR12","doi-asserted-by":"publisher","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: A tool for configurable software verification. In: Proc. CAV. pp. 184\u2013190. LNCS\u00a06806, Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"7_CR13","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Kr\u00f6ning, D., Lerda, F.: A tool for checking ANSI-C programs. In: Proc. TACAS. pp. 168\u2013176. LNCS\u00a02988, Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"7_CR14","doi-asserted-by":"publisher","unstructured":"Gadelha, M.R., Monteiro, F.R., Morse, J., Cordeiro, L.C., Fischer, B., Nicole, D.A.: ESBMC 5.0: An industrial-strength C model checker. In: Proc. ASE. pp. 888\u2013891. ACM (2018). https:\/\/doi.org\/10.1145\/3238147.3240481","DOI":"10.1145\/3238147.3240481"},{"key":"7_CR15","doi-asserted-by":"publisher","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Proc. CAV. pp. 36\u201352. LNCS\u00a08044, Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_2","DOI":"10.1007\/978-3-642-39799-8_2"},{"key":"7_CR16","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proc. OSDI. pp. 209\u2013224. USENIX Association (2008). https:\/\/dl.acm.org\/doi\/10.5555\/1855741.1855756"},{"key":"7_CR17","doi-asserted-by":"publisher","unstructured":"Rakamari\u0107, Z., Emmi, M.: SMACK: Decoupling source language details from verifier implementations. In: Proc. CAV. pp. 106\u2013113. LNCS\u00a08559, Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_7","DOI":"10.1007\/978-3-319-08867-9_7"},{"key":"7_CR18","doi-asserted-by":"publisher","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Proc. CAV. pp. 343\u2013361. LNCS\u00a09206, Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_20","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"7_CR19","doi-asserted-by":"publisher","unstructured":"Mukherjee, R., Tautschnig, M., Kroening, D.: v2c: A Verilog to C translator. In: Proc. TACAS. pp. 580\u2013586. LNCS\u00a09636, Springer (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_38","DOI":"10.1007\/978-3-662-49674-9_38"},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"Irfan, A., Cimatti, A., Griggio, A., Roveri, M., Sebastiani, R.: Verilog2SMV: A tool for word-level verification. In: Proc. DATE. pp. 1156\u20131159 (2016), https:\/\/ieeexplore.ieee.org\/document\/7459485","DOI":"10.3850\/9783981537079_0765"},{"key":"7_CR21","doi-asserted-by":"publisher","unstructured":"Minhas, M., Hasan, O., Saghar, K.: Ver2Smv: A tool for automatic Verilog to SMV translation for verifying digital circuits. In: Proc. ICEET. pp.\u00a01\u20135 (2018). https:\/\/doi.org\/10.1109\/ICEET1.2018.8338617","DOI":"10.1109\/ICEET1.2018.8338617"},{"key":"7_CR22","doi-asserted-by":"publisher","unstructured":"IEEE standard for Verilog hardware description language (2006). https:\/\/doi.org\/10.1109\/IEEESTD.2006.99495","DOI":"10.1109\/IEEESTD.2006.99495"},{"key":"7_CR23","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An open-source tool for symbolic model checking. In: Proc. CAV. pp. 359\u2013364. LNCS\u00a02404, Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_29","DOI":"10.1007\/3-540-45657-0_29"},{"key":"7_CR24","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Competition on software verification and witness validation: SV-COMP 2023. In: Proc. TACAS\u00a0(2). pp. 495\u2013522. LNCS\u00a013994, Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_29","DOI":"10.1007\/978-3-031-30820-8_29"},{"key":"7_CR25","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. Tech. rep., University of Iowa (2010), https:\/\/smtlib.cs.uiowa.edu\/papers\/smt-lib-reference-v2.0-r10.12.21.pdf"},{"key":"7_CR26","unstructured":"Niemetz, A., Preiner, M., Wolf, C., Biere, A.: Source-code repository of Btor2, BtorMC, and Boolector 3.0. https:\/\/github.com\/Boolector\/btor2tools, accessed: 2023-01-29"},{"key":"7_CR27","doi-asserted-by":"publisher","unstructured":"Beyer, D., Spiessl, M.: MetaVal: Witness validation via verification. In: Proc. CAV. pp. 165\u2013177. LNCS\u00a012225, Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_10","DOI":"10.1007\/978-3-030-53291-8_10"},{"key":"7_CR28","doi-asserted-by":"publisher","unstructured":"Beyer, D., Kanav, S.: CoVeriTeam: On-demand composition of cooperative verification systems. In: Proc. TACAS. pp. 561\u2013579. LNCS\u00a013243, Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_31","DOI":"10.1007\/978-3-030-99524-9_31"},{"key":"7_CR29","doi-asserted-by":"publisher","unstructured":"Yu, E., Biere, A., Heljanko, K.: Progress in certifying hardware model checking results. In: Proc. CAV. pp. 363\u2013386. LNCS\u00a012760, Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_17","DOI":"10.1007\/978-3-030-81688-9_17"},{"key":"7_CR30","doi-asserted-by":"publisher","unstructured":"Yu, E., Froleyks, N., Biere, A., Heljanko, K.: Stratified certification for k-induction. In: Proc. FMCAD. pp. 59\u201364. IEEE (2022). https:\/\/doi.org\/10.34727\/2022\/isbn.978-3-85448-053-2_11","DOI":"10.34727\/2022\/isbn.978-3-85448-053-2_11"},{"key":"7_CR31","doi-asserted-by":"publisher","unstructured":"Yu, E., Froleyks, N., Biere, A., Heljanko, K.: Towards compositional hardware model checking certification. In: Proc. FMCAD. pp. 1\u201311. IEEE (2023). https:\/\/doi.org\/10.34727\/2023\/ISBN.978-3-85448-060-0_12","DOI":"10.34727\/2023\/ISBN.978-3-85448-060-0_12"},{"key":"7_CR32","doi-asserted-by":"publisher","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking safety properties using induction and a SAT-solver. In: Proc. FMCAD, pp. 127\u2013144. LNCS\u00a01954, Springer (2000). https:\/\/doi.org\/10.1007\/3-540-40922-X_8","DOI":"10.1007\/3-540-40922-X_8"},{"key":"7_CR33","doi-asserted-by":"publisher","unstructured":"Froleyks, N., Heule, M., Iser, M., J\u00e4rvisalo, M., Suda, M.: SAT competition 2020. Artif. Intell. 301, 103572:1\u2013103572:25 (2021). https:\/\/doi.org\/10.1016\/j.artint.2021.103572","DOI":"10.1016\/j.artint.2021.103572"},{"key":"7_CR34","doi-asserted-by":"crossref","unstructured":"J\u00e4rvisalo, M., Berre, D.L., Roussel, O., Simon, L.: The international SAT solver competitions. AI Magazine 33(1) (2012). https:\/\/doi.org\/10.1609\/aimag.v33i1.2395","DOI":"10.1609\/aimag.v33i1.2395"},{"key":"7_CR35","doi-asserted-by":"publisher","unstructured":"Heule, M.J.H.: The DRAT format and DRAT-trim checker. CoRR 1610(06229) (October 2016). https:\/\/doi.org\/10.48550\/arXiv.1610.06229","DOI":"10.48550\/arXiv.1610.06229"},{"key":"7_CR36","doi-asserted-by":"publisher","unstructured":"Lammich, P.: Efficient verified (UN)SAT certificate checking. J. Autom. Reason. 64(3), 513\u2013532 (2020). https:\/\/doi.org\/10.1007\/s10817-019-09525-z","DOI":"10.1007\/s10817-019-09525-z"},{"key":"7_CR37","doi-asserted-by":"publisher","unstructured":"Wetzler, N., Heule, M.J.H., Jr., W.A.H.: DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In: Proc. SAT. pp. 422\u2013429. LNCS\u00a08561, Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-09284-3_31","DOI":"10.1007\/978-3-319-09284-3_31"},{"key":"7_CR38","unstructured":"Bury, G., Bobot, F.: Verifying models with Dolmen. In: Proc. SMT Workshop. CEUR Workshop Proceedings, CEUR (2023). https:\/\/ceur-ws.org\/Vol-3429\/short9.pdf"},{"key":"7_CR39","doi-asserted-by":"publisher","unstructured":"Niemetz, A., Preiner, M., Lonsing, F., Seidl, M., Biere, A.: Resolution-based certificate extraction for QBF - (tool presentation). In: Proc. SAT. pp. 430\u2013435. LNCS\u00a07317, Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_33","DOI":"10.1007\/978-3-642-31612-8_33"},{"key":"7_CR40","doi-asserted-by":"publisher","unstructured":"Balabanov, V., Jiang, J.H.R.: Unified QBF certification and its applications. Formal Methods Syst. Des. 41(1), 45\u201365 (2012). https:\/\/doi.org\/10.1007\/s10703-012-0152-6","DOI":"10.1007\/s10703-012-0152-6"},{"key":"7_CR41","doi-asserted-by":"publisher","unstructured":"Namjoshi, K.S.: Certifying model checkers. In: Proc. CAV. pp. 2\u201313. LNCS\u00a02102, Springer (2001). https:\/\/doi.org\/10.1007\/3-540-44585-4_2","DOI":"10.1007\/3-540-44585-4_2"},{"key":"7_CR42","doi-asserted-by":"publisher","unstructured":"Giesl, J., Mesnard, F., Rubio, A., Thiemann, R., Waldmann, J.: Termination competition (termCOMP 2015). In: Proc. CADE. pp. 105\u2013108. LNCS\u00a09195, Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_6","DOI":"10.1007\/978-3-319-21401-6_6"},{"key":"7_CR43","doi-asserted-by":"publisher","unstructured":"Sternagel, C., Thiemann, R.: The certification problem format. In: Proc. UITP. pp. 61\u201372. EPTCS\u00a0167, EPTCS (2014). https:\/\/doi.org\/10.4204\/EPTCS.167.8","DOI":"10.4204\/EPTCS.167.8"},{"key":"7_CR44","doi-asserted-by":"publisher","unstructured":"Griggio, A., Roveri, M., Tonetta, S.: Certifying proofs for LTL model checking. In: Proc. FMCAD. pp.\u00a01\u20139. IEEE (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8603022","DOI":"10.23919\/FMCAD.2018.8603022"},{"key":"7_CR45","doi-asserted-by":"publisher","unstructured":"Kahsai, T., Tinelli, C.: PKind: A parallel k-induction based model checker. In: Proc. Int. Workshop on Parallel and Distributed Methods in Verification. pp. 55\u201362. EPTCS\u00a072, EPTCS (2011). https:\/\/doi.org\/10.4204\/EPTCS.72.6","DOI":"10.4204\/EPTCS.72.6"},{"key":"7_CR46","doi-asserted-by":"publisher","unstructured":"Beyer, D., Spiessl, M.: LIV: A loop-invariant validation using straight-line programs. In: Proc. ASE. pp. 2074\u20132077. IEEE (2023). https:\/\/doi.org\/10.1109\/ASE56229.2023.00214","DOI":"10.1109\/ASE56229.2023.00214"},{"key":"7_CR47","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Lemberger, T., Tautschnig, M.: Tests from witnesses: Execution-based validation of verification results. In: Proc. TAP. pp. 3\u201323. LNCS\u00a010889, Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-92994-1_1","DOI":"10.1007\/978-3-319-92994-1_1"},{"key":"7_CR48","doi-asserted-by":"publisher","unstructured":"Case, M.L., Mony, H., Baumgartner, J., Kanzelman, R.: Enhanced verification by temporal decomposition. In: Proc. FMCAD. pp. 17\u201324. IEEE (2009). https:\/\/doi.org\/10.1109\/FMCAD.2009.5351146","DOI":"10.1109\/FMCAD.2009.5351146"},{"key":"7_CR49","doi-asserted-by":"publisher","unstructured":"Biere, A.: The AIGER And-Inverter Graph (AIG) format version 20071012. Tech. Rep.\u00a007\/1, Institute for Formal Models and Verification, Johannes Kepler University (2007). https:\/\/doi.org\/10.35011\/fmvtr.2007-1","DOI":"10.35011\/fmvtr.2007-1"},{"key":"7_CR50","doi-asserted-by":"publisher","unstructured":"Brayton, R., Mishchenko, A.: ABC: An academic industrial-strength verification tool. In: Proc. CAV. pp. 24\u201340. LNCS\u00a06174, Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_5","DOI":"10.1007\/978-3-642-14295-6_5"},{"key":"7_CR51","doi-asserted-by":"publisher","unstructured":"Goel, A., Sakallah, K.: AVR: Abstractly verifying reachability. In: Proc. TACAS. pp. 413\u2013422. LNCS\u00a012078, Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_23","DOI":"10.1007\/978-3-030-45190-5_23"},{"key":"7_CR52","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Verifiers and validators of the 12th Intl. Competition on Software Verification (SV-COMP 2023). Zenodo (2023). https:\/\/doi.org\/10.5281\/zenodo.7627829","DOI":"10.5281\/zenodo.7627829"},{"key":"7_CR53","doi-asserted-by":"publisher","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Reliable benchmarking: Requirements and solutions. Int. J. Softw. Tools Technol. Transfer 21(1), 1\u201329 (2019). https:\/\/doi.org\/10.1007\/s10009-017-0469-y","DOI":"10.1007\/s10009-017-0469-y"},{"key":"7_CR54","unstructured":"E\u00e9n, N., Mishchenko, A., Brayton, R.K.: Efficient implementation of property directed reachability. In: Proc. FMCAD. pp. 125\u2013134. FMCAD Inc. (2011). https:\/\/dl.acm.org\/doi\/10.5555\/2157654.2157675"},{"key":"7_CR55","doi-asserted-by":"publisher","unstructured":"Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. J.\u00a0Symb. Log. 22(3), 250\u2013268 (1957). https:\/\/doi.org\/10.2307\/2963593","DOI":"10.2307\/2963593"},{"key":"7_CR56","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Proc. CAV. pp. 1\u201313. LNCS\u00a02725, Springer (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_1","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"7_CR57","doi-asserted-by":"publisher","unstructured":"Beyer, D., Lee, N.Z., Wendler, P.: Interpolation and SAT-based model checking revisited: Adoption to software verification. arXiv\/CoRR 2208(05046) (July 2022). https:\/\/doi.org\/10.48550\/arXiv.2208.05046","DOI":"10.48550\/arXiv.2208.05046"},{"key":"7_CR58","doi-asserted-by":"publisher","unstructured":"Vizel, Y., Grumberg, O.: Interpolation-sequence based model checking. In: Proc. FMCAD. pp.\u00a01\u20138. IEEE (2009). https:\/\/doi.org\/10.1109\/FMCAD.2009.5351148","DOI":"10.1109\/FMCAD.2009.5351148"},{"key":"7_CR59","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Proc. CAV. pp. 123\u2013136. LNCS\u00a04144, Springer (2006). https:\/\/doi.org\/10.1007\/11817963_14","DOI":"10.1007\/11817963_14"},{"key":"7_CR60","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Proc. POPL. pp. 232\u2013244. ACM (2004). https:\/\/doi.org\/10.1145\/964001.964021","DOI":"10.1145\/964001.964021"},{"key":"7_CR61","doi-asserted-by":"publisher","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Proc. TACAS. pp. 193\u2013207. LNCS\u00a01579, Springer (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14","DOI":"10.1007\/3-540-49059-0_14"},{"key":"7_CR62","doi-asserted-by":"crossref","unstructured":"\u00c1d\u00e1m, Z., Beyer, D., Chien, P.C., Lee, N.Z., Sirrenberg, N.: Supplementary webpage for TACAS\u00a02024 article \u2018Btor2-Cert: A certifying hardware-verification framework using software analyzers\u2019. https:\/\/www.sosy-lab.org\/research\/btor2-cert\/","DOI":"10.1007\/978-3-031-57256-2_7"},{"key":"7_CR63","doi-asserted-by":"publisher","unstructured":"\u00c1d\u00e1m, Z., Beyer, D., Chien, P.C., Lee, N.Z., Sirrenberg, N.: Reproduction package for TACAS\u00a02024 article \u2018Btor2-Cert: A certifying hardware-verification framework using software analyzers\u2019. Zenodo (2023). https:\/\/doi.org\/10.5281\/zenodo.10548597","DOI":"10.5281\/zenodo.10548597"},{"key":"7_CR64","doi-asserted-by":"publisher","unstructured":"\u00c1d\u00e1m, Z., Beyer, D., Chien, P.C., Lee, N.Z., Sirrenberg, N.: Reproduction package for TACAS\u00a02024 submission \u2018Btor2-Cert: A certifying hardware-verification framework using software analyzers\u2019. Zenodo (2023). https:\/\/doi.org\/10.5281\/zenodo.10013059","DOI":"10.5281\/zenodo.10013059"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-57256-2_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,15]],"date-time":"2024-11-15T17:21:20Z","timestamp":1731691280000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57256-2_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572555","9783031572562"],"references-count":64,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57256-2_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"5 April 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"159","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"53","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}