{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T20:55:08Z","timestamp":1777582508308,"version":"3.51.4"},"publisher-location":"Cham","reference-count":71,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031308192","type":"print"},{"value":"9783031308208","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,20]],"date-time":"2023-04-20T00:00:00Z","timestamp":1681948800000},"content-version":"vor","delay-in-days":109,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Across the broad research field concerned with the analysis of computational systems, research endeavors are often categorized by the respective models under investigation. Algorithms and tools are usually developed for a specific model, hindering their applications to similar problems originating from other computational systems. A prominent example of such a situation is the area of formal verification and testing for hardware and software systems. The two research communities share common theoretical foundations and solving methods, including satisfiability, interpolation, and abstraction refinement. Nevertheless, it is often demanding for one community to benefit from the advancements of the other, as analyzers typically assume a particular input format. To bridge the gap between the hardware and software analysis, we propose <jats:sc>Btor2C<\/jats:sc>, a translator from word-level sequential circuits to C\u00a0programs. We choose the <jats:sc>Btor2<\/jats:sc> language as the input format for its simplicity and bit-precise semantics. It can be deemed as an <jats:italic>intermediate representation<\/jats:italic> tailored for analysis. Given a <jats:sc>Btor2<\/jats:sc> circuit, <jats:sc>Btor2C<\/jats:sc> generates a behaviorally equivalent program in the language\u00a0C, supported by many static program analyzers. We demonstrate the use cases of <jats:sc>Btor2C<\/jats:sc> by translating the benchmark set from the Hardware Model Checking Competitions into C programs and analyze them by tools from the Intl. Competitions on Software Verification and Testing. Our results show that software analyzers can complement hardware verifiers for enhanced quality assurance: For example, the software verifier\u00a0<jats:sc>VeriAbs<\/jats:sc> with\u00a0<jats:sc>Btor2C<\/jats:sc> as preprocessor found more bugs than the best hardware verifiers\u00a0<jats:sc>ABC<\/jats:sc> and\u00a0<jats:sc>AVR<\/jats:sc> in our experiment.<\/jats:p>","DOI":"10.1007\/978-3-031-30820-8_12","type":"book-chapter","created":{"date-parts":[[2023,4,19]],"date-time":"2023-04-19T19:02:36Z","timestamp":1681930956000},"page":"152-172","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Bridging Hardware and Software Analysis with Btor2C: A Word-Level-Circuit-to-C Translator"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4832-7662","authenticated-orcid":false,"given":"Dirk","family":"Beyer","sequence":"first","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"}]}],"member":"297","published-online":{"date-parts":[[2023,4,20]]},"reference":[{"key":"12_CR1","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":"12_CR2","doi-asserted-by":"publisher","unstructured":"Afzal, M., Asia, A., Chauhan, A., Chimdyalwar, B., Darke, P., Datar, A., Kumar, S., Venkatesh, R.: VeriAbs: Verification by abstraction and test generation. In: Proc. ASE. pp. 1138\u20131141 (2019). https:\/\/doi.org\/10.1109\/ASE.2019.00121","DOI":"10.1109\/ASE.2019.00121"},{"key":"12_CR3","doi-asserted-by":"publisher","unstructured":"Alshmrany, K.M., Aldughaim, M., Bhayat, A., Cordeiro, L.C.: FuSeBMC: An energy-efficient test generator for finding security vulnerabilities in C programs. In: Proc. TAP. pp. 85\u2013105. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-79379-1_6","DOI":"10.1007\/978-3-030-79379-1_6"},{"key":"12_CR4","doi-asserted-by":"publisher","unstructured":"Ball, T., Cook, B., Levin, V., Rajamani, S.K.: Slam and Static Driver Verifier: Technology transfer of formal methods inside Microsoft. In: Proc. IFM. pp. 1\u201320. LNCS\u00a02999, Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-24756-2_1","DOI":"10.1007\/978-3-540-24756-2_1"},{"key":"12_CR5","doi-asserted-by":"publisher","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Proc. PLDI. pp. 203\u2013213. ACM (2001). https:\/\/doi.org\/10.1145\/378795.378846","DOI":"10.1145\/378795.378846"},{"key":"12_CR6","unstructured":"Ball, T., Rajamani, S.K.: Boolean programs: A model and process for software analysis. Tech. Rep. MSR Tech. Rep. 2000-14, Microsoft Research (2000), https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/tr-2000-14.pdf"},{"key":"12_CR7","doi-asserted-by":"publisher","unstructured":"Ball, T., Rajamani, S.K.: The Slam project: Debugging system software via static analysis. In: Proc. POPL. pp.\u00a01\u20133. ACM (2002). https:\/\/doi.org\/10.1145\/503272.503274","DOI":"10.1145\/503272.503274"},{"key":"12_CR8","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":"12_CR9","doi-asserted-by":"publisher","unstructured":"Barrett, C., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Model Checking, pp. 305\u2013343. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_11","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"12_CR10","doi-asserted-by":"publisher","unstructured":"Beckert, B., H\u00e4hnle, R.: Reasoning and verification: State of the art and current trends. IEEE Intelligent Systems 29(1), 20\u201329 (2014). https:\/\/doi.org\/10.1109\/MIS.2014.3","DOI":"10.1109\/MIS.2014.3"},{"key":"12_CR11","unstructured":"Beyer, D.: 11th Intl. Competition on Software Verification (SV-COMP 2022). https:\/\/sv-comp.sosy-lab.org\/2022\/, accessed: 2023-01-29"},{"key":"12_CR12","unstructured":"Beyer, D.: 4th Intl. Competition on Software Testing (Test-Comp 2022). https:\/\/test-comp.sosy-lab.org\/2022\/, accessed: 2023-01-29"},{"key":"12_CR13","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Advances in automatic software testing: Test-Comp 2022. In: Proc. FASE. pp. 321\u2013335. LNCS\u00a013241, Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99429-7_18","DOI":"10.1007\/978-3-030-99429-7_18"},{"key":"12_CR14","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Progress on software verification: SV-COMP 2022. In: Proc. TACAS\u00a0(2). pp. 375\u2013402. LNCS\u00a013244, Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_20","DOI":"10.1007\/978-3-030-99527-0_20"},{"key":"12_CR15","doi-asserted-by":"publisher","unstructured":"Beyer, D., Chien, P.C., Lee, N.Z.: Reproduction package for TACAS\u00a02023 submission \u2018Bridging hardware and software analysis with Btor2C: A word-level-circuit-to-C translator\u2019. Zenodo (2022). https:\/\/doi.org\/10.5281\/zenodo.7303732","DOI":"10.5281\/zenodo.7303732"},{"key":"12_CR16","doi-asserted-by":"publisher","unstructured":"Beyer, D., Chien, P.C., Lee, N.Z.: Reproduction package for TACAS\u00a02023 article \u2018Bridging hardware and software analysis with Btor2C: A word-level-circuit-to-C translator\u2019. Zenodo (2023). https:\/\/doi.org\/10.5281\/zenodo.7551707","DOI":"10.5281\/zenodo.7551707"},{"key":"12_CR17","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Wendler, P.: Boosting k-induction with continuously-refined invariants. In: Proc. CAV. pp. 622\u2013640. LNCS\u00a09206, Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_42","DOI":"10.1007\/978-3-319-21690-4_42"},{"key":"12_CR18","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Wendler, P.: A unifying view on SMT-based software verification. J. Autom. Reasoning 60(3), 299\u2013335 (2018). https:\/\/doi.org\/10.1007\/s10817-017-9432-6","DOI":"10.1007\/s10817-017-9432-6"},{"key":"12_CR19","doi-asserted-by":"publisher","unstructured":"Beyer, D., Gulwani, S., Schmidt, D.: Combining model checking and data-flow analysis. In: Handbook of Model Checking, pp. 493\u2013540. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_16","DOI":"10.1007\/978-3-319-10575-8_16"},{"key":"12_CR20","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":"12_CR21","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":"12_CR22","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":"12_CR23","doi-asserted-by":"publisher","unstructured":"Beyer, D., Petrenko, A.K.: Linux driver verification. In: Proc. ISoLA. pp.\u00a01\u20136. LNCS\u00a07610, Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-34032-1_1","DOI":"10.1007\/978-3-642-34032-1_1"},{"key":"12_CR24","unstructured":"Beyer, D., Wendler, P.: Algorithms for software model checking: Predicate abstraction vs. Impact. In: Proc. FMCAD. pp. 106\u2013113. FMCAD (2012), https:\/\/www.sosy-lab.org\/research\/pub\/2012-FMCAD.Algorithms_for_Software_Model_Checking.pdf"},{"key":"12_CR25","doi-asserted-by":"publisher","unstructured":"Beyer, D., Podelski, A.: Software model checking: 20 years and beyond. In: Principles of Systems Design. pp. 554\u2013582. LNCS\u00a013660, Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-22337-2_27","DOI":"10.1007\/978-3-031-22337-2_27"},{"key":"12_CR26","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":"12_CR27","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":"12_CR28","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":"12_CR29","unstructured":"Biere, A., Froleyks, N., Preiner, M.: 11th Hardware Model Checking Competition (HWMCC 2020). http:\/\/fmv.jku.at\/hwmcc20\/, accessed: 2023-01-29"},{"key":"12_CR30","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":"12_CR31","doi-asserted-by":"publisher","unstructured":"Brummayer, R., Biere, A., Lonsing, F.: Btor: Bit-precise modelling of word-level problems for model checking. In: Proc. SMT\/BPR. pp. 33\u201338. ACM (2008). https:\/\/doi.org\/10.1145\/1512464.1512472","DOI":"10.1145\/1512464.1512472"},{"key":"12_CR32","doi-asserted-by":"publisher","unstructured":"Calcagno, C., Distefano, D., Dubreil, J., Gabi, D., Hooimeijer, P., Luca, M., O\u2019Hearn, P.W., Papakonstantinou, I., Purbrick, J., Rodriguez, D.: Moving fast with software verification. In: Proc. NFM. pp. 3\u201311. LNCS\u00a09058, Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-17524-9_1","DOI":"10.1007\/978-3-319-17524-9_1"},{"key":"12_CR33","doi-asserted-by":"publisher","unstructured":"Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuxmv symbolic model checker. In: Proc. CAV. pp. 334\u2013342. LNCS\u00a08559, Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"12_CR34","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":"12_CR35","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Proc. TACAS. pp. 93\u2013107. LNCS\u00a07795, Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"12_CR36","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752\u2013794 (2003). https:\/\/doi.org\/10.1145\/876638.876643","DOI":"10.1145\/876638.876643"},{"key":"12_CR37","doi-asserted-by":"publisher","unstructured":"Cook, B.: Formal reasoning about the security of Amazon web services. In: Proc. CAV\u00a0(2). pp. 38\u201347. LNCS\u00a010981, Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_3","DOI":"10.1007\/978-3-319-96145-3_3"},{"key":"12_CR38","doi-asserted-by":"publisher","unstructured":"Darke, P., Chimdyalwar, B., Venkatesh, R., Shrotri, U., Metta, R.: Over-approximating loops to prove properties using bounded model checking. In: Proc. DATE. pp. 1407\u20131412. IEEE (2015). https:\/\/doi.org\/10.7873\/DATE.2015.0245","DOI":"10.7873\/DATE.2015.0245"},{"key":"12_CR39","doi-asserted-by":"publisher","unstructured":"Donaldson, A.F., Haller, L., Kr\u00f6ning, D., R\u00fcmmer, P.: Software verification using k-induction. In: Proc. SAS. pp. 351\u2013368. LNCS\u00a06887, Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-23702-7_26","DOI":"10.1007\/978-3-642-23702-7_26"},{"key":"12_CR40","doi-asserted-by":"publisher","unstructured":"Dutertre, B.: Yices 2.2. In: Proc. CAV. pp. 737\u2013744. LNCS\u00a08559, Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"12_CR41","unstructured":"E\u00e9n, N., Mishchenko, A., Brayton, R.K.: Efficient implementation of property directed reachability. In: Proc. FMCAD. pp. 125\u2013134. FMCAD Inc. (2011), http:\/\/dl.acm.org\/citation.cfm?id=2157675"},{"key":"12_CR42","doi-asserted-by":"publisher","unstructured":"Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: Proc. POPL. pp. 191\u2013202. ACM (2002). https:\/\/doi.org\/10.1145\/503272.503291","DOI":"10.1145\/503272.503291"},{"key":"12_CR43","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":"12_CR44","doi-asserted-by":"publisher","unstructured":"Gadelha, M.Y., Ismail, H.I., Cordeiro, L.C.: Handling loops in bounded model checking of C programs via k-induction. Int. J. Softw. Tools Technol. Transf. 19(1), 97\u2013114 (February 2017). https:\/\/doi.org\/10.1007\/s10009-015-0407-9","DOI":"10.1007\/s10009-015-0407-9"},{"key":"12_CR45","doi-asserted-by":"publisher","unstructured":"Goel, A., Sakallah, K.: Model checking of Verilog RTL using IC3 with syntax-guided abstraction. In: Proc. NFM. pp. 166\u2013185. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-20652-9_11","DOI":"10.1007\/978-3-030-20652-9_11"},{"key":"12_CR46","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":"12_CR47","doi-asserted-by":"publisher","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with Pvs. In: Proc. CAV. pp. 72\u201383. LNCS\u00a01254, Springer (1997). https:\/\/doi.org\/10.1007\/3-540-63166-6_10","DOI":"10.1007\/3-540-63166-6_10"},{"key":"12_CR48","doi-asserted-by":"publisher","unstructured":"Greaves, D.J.: A Verilog to C compiler. In: Proc. RSP. pp. 122\u2013127. IEEE (2000). https:\/\/doi.org\/10.1109\/IWRSP.2000.855208","DOI":"10.1109\/IWRSP.2000.855208"},{"key":"12_CR49","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":"12_CR50","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proc. POPL. pp. 58\u201370. ACM (2002). https:\/\/doi.org\/10.1145\/503272.503279","DOI":"10.1145\/503272.503279"},{"key":"12_CR51","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":"12_CR52","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":"12_CR53","doi-asserted-by":"publisher","unstructured":"Jhala, R., Majumdar, R.: Software model checking. ACM Computing Surveys 41(4) (2009). https:\/\/doi.org\/10.1145\/1592434.1592438","DOI":"10.1145\/1592434.1592438"},{"key":"12_CR54","doi-asserted-by":"publisher","unstructured":"Khoroshilov, A.V., Mutilin, V.S., Petrenko, A.K., Zakharov, V.: Establishing Linux driver verification process. In: Proc. Ershov Memorial Conference. pp. 165\u2013176. LNCS\u00a05947, Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-11486-1_14","DOI":"10.1007\/978-3-642-11486-1_14"},{"key":"12_CR55","unstructured":"Kroening, D., Purandare, M.: EBMC. http:\/\/www.cprover.org\/ebmc\/, accessed: 2023-01-29"},{"key":"12_CR56","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: Symbolic Model Checking. Springer (1993). https:\/\/doi.org\/10.1007\/978-1-4615-3190-6","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"12_CR57","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":"12_CR58","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":"12_CR59","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":"12_CR60","doi-asserted-by":"publisher","unstructured":"Mukherjee, R., Kroening, D., Melham, T.: Hardware verification using software analyzers. In: Proc. ISVLSI. pp. 7\u201312. IEEE (2015). https:\/\/doi.org\/10.1109\/ISVLSI.2015.107","DOI":"10.1109\/ISVLSI.2015.107"},{"key":"12_CR61","doi-asserted-by":"crossref","unstructured":"Mukherjee, R., Schrammel, P., Kroening, D., Melham, T.: Unbounded safety verification for hardware using software analyzers. In: Proc. DATE. pp. 1152\u20131155. IEEE (2016), https:\/\/ieeexplore.ieee.org\/document\/7459484","DOI":"10.3850\/9783981537079_0274"},{"key":"12_CR62","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":"12_CR63","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":"12_CR64","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":"12_CR65","doi-asserted-by":"publisher","unstructured":"Pel\u00e1nek, R.: BEEM: Benchmarks for explicit model checkers. In: Proc. SPIN. pp. 263\u2013267. LNCS\u00a04595, Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-73370-6_17","DOI":"10.1007\/978-3-540-73370-6_17"},{"key":"12_CR66","doi-asserted-by":"publisher","unstructured":"Richter, C., H\u00fcllermeier, E., Jakobs, M.C., Wehrheim, H.: Algorithm selection for software validation based on graph kernels. Autom. Softw. Eng. 27(1), 153\u2013186 (2020). https:\/\/doi.org\/10.1007\/s10515-020-00270-x","DOI":"10.1007\/s10515-020-00270-x"},{"key":"12_CR67","unstructured":"Rozier, K.Y., Shankar, N., Tinelli, C., Vardi, M.: An open-source, state-of-the-art symbolic model-checking framework for the model-checking research community. https:\/\/www.aere.iastate.edu\/modelchecker\/, accessed: 2023-01-29"},{"key":"12_CR68","unstructured":"Snyder, W.: Verilator. https:\/\/www.veripool.org\/verilator\/, accessed: 2023-01-29"},{"key":"12_CR69","unstructured":"Wahl, T.: The k-induction principle (2013), http:\/\/www.ccs.neu.edu\/home\/wahl\/Publications\/k-induction.pdf"},{"key":"12_CR70","unstructured":"Wolf, C.: Yosys open synthesis suite. https:\/\/yosyshq.net\/yosys\/, accessed: 2023-01-29"},{"key":"12_CR71","doi-asserted-by":"publisher","unstructured":"Yeh, H., Wu, C., Huang, C.R.: QuteRTL: Towards an open source framework for RTL design synthesis and verification. In: Proc. TACAS. pp. 377\u2013391. LNCS\u00a07214, Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_26","DOI":"10.1007\/978-3-642-28756-5_26"}],"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-30820-8_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,2]],"date-time":"2023-08-02T11:03:55Z","timestamp":1690974235000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30820-8_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308192","9783031308208"],"references-count":71,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30820-8_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"20 April 2023","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":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/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":"169","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":"56","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":"6","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":"11","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)"}}]}}