{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:16:16Z","timestamp":1784837776133,"version":"3.55.0"},"publisher-location":"Cham","reference-count":144,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031757778","type":"print"},{"value":"9783031757785","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,11,18]],"date-time":"2024-11-18T00:00:00Z","timestamp":1731888000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,11,18]],"date-time":"2024-11-18T00:00:00Z","timestamp":1731888000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Transformation plays a key role in verification technology, conveying information across different abstraction layers\u00a0and underpinning the correctness, efficiency, and usability of formal-methods tools. Nevertheless, transformation procedures are often tightly coupled with individual verifiers, and thus, hard to reuse across different tools. The lack of modularity incurs repeated engineering effort\u00a0and the risk of bugs in the process of \u2018reinventing the wheel\u2019. It can be seen as a new paradigm to construct verification technology by employing standardized formats and interfaces for information exchange,\u00a0and by building modular transformers between verification artifacts. Following this paradigm of <jats:italic>modular transformation<\/jats:italic>, recent works\u00a0have (1)\u00a0enhanced and complemented the state of the art by transforming verification\u00a0tasks and applying tools for other modeling languages or specifications, (2)\u00a0built new tools by combining mature ones via standardized formats for exchanging verification artifacts,\u00a0and (3)\u00a0communicated certificates of verification results to improve usability and explainability. In this paper, we survey existing transformation procedures\u00a0and advocate the paradigm of modular transformation and exchange formats. Our vision is an ecosystem of reusable verification components\u00a0that supports joining forces of all available techniques, allows agile development of new tools,\u00a0and provides a common ground to evaluate and compare future scientific advancements: via modular transformation.<\/jats:p>","DOI":"10.1007\/978-3-031-75778-5_9","type":"book-chapter","created":{"date-parts":[[2024,11,17]],"date-time":"2024-11-17T12:09:29Z","timestamp":1731845369000},"page":"175-205","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["The Transformation Game: Joining Forces for\u00a0Verification"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4832-7662","authenticated-orcid":false,"given":"Dirk","family":"Beyer","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8096-5595","authenticated-orcid":false,"given":"Nian-Ze","family":"Lee","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,11,18]]},"reference":[{"key":"9_CR1","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT (2008), https:\/\/www.worldcat.org\/isbn\/978-0-262-02649-9"},{"key":"9_CR2","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":"9_CR3","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":"9_CR4","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":"9_CR5","doi-asserted-by":"publisher","unstructured":"Calcagno, C., Distefano, D., Dubreil, J., Gabi, D., Hooimeijer, P., Luca, M., O\u2019Hearn, P., 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":"9_CR6","unstructured":"Li, X., Li, X., Dall, C., Gu, R., Nieh, J., Sait, Y., Stockwell, G.: Design and verification of the Arm confidential compute architecture. In: Proc. OSDI. pp. 465\u2013484. USENIX Association (2022), https:\/\/www.usenix.org\/system\/files\/osdi22-li.pdf"},{"issue":"OOPSLA1","key":"9_CR7","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1145\/3586040","volume":"7","author":"ACJ Fox","year":"2023","unstructured":"Fox, A.C.J., Stockwell, G., Xiong, S., Becker, H., Mulligan, D.P., Petri, G., Chong, N.: A verification methodology for the Arm confidential computing architecture: From a secure specification to safe implementations. Proc. ACM Program. Lang. 7(OOPSLA1), 376\u2013405 (2023). https:\/\/doi.org\/10.1145\/3586040","journal-title":"Proc. ACM Program. Lang."},{"key":"9_CR8","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol.\u00a0185. IOS (2009)"},{"key":"9_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":"9_CR10","unstructured":"Kernighan, B., Ritchie, D.: The C Programming Language. Prentice Hall (1978)"},{"key":"9_CR11","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":"9_CR12","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":"9_CR13","doi-asserted-by":"publisher","unstructured":"Beyer, D., Wehrheim, H.: Verification artifacts in cooperative verification: Survey and unifying component framework. In: Proc. ISoLA\u00a0(1). pp. 143\u2013167. LNCS\u00a012476, Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-61362-4_8","DOI":"10.1007\/978-3-030-61362-4_8"},{"key":"9_CR14","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":"9_CR15","unstructured":"DeMarco, T.: Structured Analysis and System Specification. Prentice Hall, facsimile edn. (1979)"},{"key":"9_CR16","unstructured":"Szyperski, C.A., Gruntz, D., Murer, S.: Component Software: Beyond Object-Oriented Programming. Addison-Wesley, 2nd edn. (2002)"},{"issue":"7","key":"9_CR17","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/361011.361061","volume":"17","author":"D Ritchie","year":"1974","unstructured":"Ritchie, D., Thompson, K.: The UNIX time-sharing system. Commun. ACM 17(7), 365\u2013375 (1974). https:\/\/doi.org\/10.1145\/361011.361061","journal-title":"Commun. ACM"},{"key":"9_CR18","unstructured":"Raymond, E.S.: The Art of UNIX Programming. Addison-Wesley, 1st edn. (2003)"},{"key":"9_CR19","doi-asserted-by":"publisher","unstructured":"Lattner, C., Adve, V.S.: Llvm: A compilation framework for lifelong program analysis and transformation. In: Proc. CGO. pp. 75\u201388. IEEE (2004). https:\/\/doi.org\/10.1109\/CGO.2004.1281665","DOI":"10.1109\/CGO.2004.1281665"},{"key":"9_CR20","doi-asserted-by":"publisher","unstructured":"Lattner, C., Amini, M., Bondhugula, U., Cohen, A., Davis, A., Pienaar, J., Riddle, R., Shpeisman, T., Vasilache, N., Zinenko, O.: MLIR: Scaling compiler infrastructure for domain-specific computation. In: Proc. CGO. pp. 2\u201314. IEEE (2021). https:\/\/doi.org\/10.1109\/CGO51591.2021.9370308","DOI":"10.1109\/CGO51591.2021.9370308"},{"key":"9_CR21","doi-asserted-by":"publisher","unstructured":"Beyer, D., Haltermann, J., Lemberger, T., Wehrheim, H.: Decomposing software verification into off-the-shelf components: An application to CEGAR. In: Proc. ICSE. pp. 536\u2013548. ACM (2022). https:\/\/doi.org\/10.1145\/3510003.3510064","DOI":"10.1145\/3510003.3510064"},{"key":"9_CR22","doi-asserted-by":"publisher","unstructured":"Beyer, D., Jakobs, M.C., Lemberger, T., Wehrheim, H.: Reducer-based construction of conditional verifiers. In: Proc. ICSE. pp. 1182\u20131193. ACM (2018). https:\/\/doi.org\/10.1145\/3180155.3180259","DOI":"10.1145\/3180155.3180259"},{"key":"9_CR23","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":"9_CR24","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":"9_CR25","doi-asserted-by":"publisher","unstructured":"Beyer, D., Lemberger, T.: Conditional testing: Off-the-shelf combination of test-case generators. In: Proc. ATVA. pp. 189\u2013208. LNCS\u00a011781, Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_11","DOI":"10.1007\/978-3-030-31784-3_11"},{"issue":"3","key":"9_CR26","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/s10009-020-00587-8","volume":"23","author":"D Beyer","year":"2021","unstructured":"Beyer, D., Jakobs, M.C.: Cooperative verifier-based testing with CoVeriTest. Int. J. Softw. Tools Technol. Transfer 23(3), 313\u2013333 (2021). https:\/\/doi.org\/10.1007\/s10009-020-00587-8","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"9_CR27","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\u00a0(2). pp. 152\u2013172. 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":"9_CR28","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":"9_CR29","doi-asserted-by":"publisher","unstructured":"Chien, P.C., Lee, N.Z.: CPV: A circuit-based program verifier (competition contribution). In: Proc. TACAS\u00a0(3). pp. 365\u2013370. LNCS\u00a014572, Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_22","DOI":"10.1007\/978-3-031-57256-2_22"},{"issue":"1","key":"9_CR30","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/j.entcs.2005.11.018","volume":"149","author":"V Schuppan","year":"2006","unstructured":"Schuppan, V., Biere, A.: Liveness checking as safety checking for infinite state spaces. Electr. Notes Theor. Comput. Sci. 149(1), 79\u201396 (2006). https:\/\/doi.org\/10.1016\/j.entcs.2005.11.018","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"9_CR31","doi-asserted-by":"publisher","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: Checking memory safety with Blast. In: Proc. FASE. pp. 2\u201318. LNCS\u00a03442, Springer (2005). https:\/\/doi.org\/10.1007\/978-3-540-31984-9_2","DOI":"10.1007\/978-3-540-31984-9_2"},{"issue":"1","key":"9_CR32","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/S10703-009-0078-9","volume":"35","author":"A Lal","year":"2009","unstructured":"Lal, A., Reps, T.W.: Reducing concurrent analysis under a context bound to sequential analysis. Formal Methods Syst. Des. 35(1), 73\u201397 (2009). https:\/\/doi.org\/10.1007\/S10703-009-0078-9","journal-title":"Formal Methods Syst. Des."},{"key":"9_CR33","doi-asserted-by":"publisher","unstructured":"\u00c1d\u00e1m, Z., Beyer, D., Chien, P.C., Lee, N.Z., Sirrenberg, N.: Btor2-Cert: A certifying hardware-verification framework using software analyzers. In: Proc. TACAS\u00a0(3). pp. 129\u2013149. LNCS\u00a014572, Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_7","DOI":"10.1007\/978-3-031-57256-2_7"},{"key":"9_CR34","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":"9_CR35","doi-asserted-by":"publisher","unstructured":"Beyer, D., Spiessl, M., Umbricht, S.: Cooperation between automatic and interactive software verifiers. In: Proc. SEFM. p. 111-128. LNCS\u00a013550, Springer (2022).https:\/\/doi.org\/10.1007\/978-3-031-17108-6_7","DOI":"10.1007\/978-3-031-17108-6_7"},{"key":"9_CR36","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":"9_CR37","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":"9_CR38","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":"9_CR39","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":"9_CR40","doi-asserted-by":"publisher","unstructured":"Garavel, H., ter Beek, M.H., van\u00a0de Pol, J.: The 2020 expert survey on formal methods. In: Proc. FMICS. pp. 3\u201369. LNCS\u00a012327, Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-58298-2_1","DOI":"10.1007\/978-3-030-58298-2_1"},{"key":"9_CR41","doi-asserted-by":"publisher","unstructured":"Alglave, J., Donaldson, A.F., Kr\u00f6ning, D., Tautschnig, M.: Making software verification tools really work. In: Proc. ATVA. pp. 28\u201342. LNCS\u00a06996, Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-24372-1_3","DOI":"10.1007\/978-3-642-24372-1_3"},{"key":"9_CR42","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":"9_CR43","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"},{"issue":"2","key":"9_CR44","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/j.cosrev.2010.09.009","volume":"5","author":"RM McConnell","year":"2011","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","journal-title":"Computer Science Review"},{"issue":"3","key":"9_CR45","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/j.tcs.2006.08.012","volume":"364","author":"F Besson","year":"2006","unstructured":"Besson, F., Jensen, T.P., Pichardie, D.: Proof-carrying code from certified abstract interpretation and fixpoint compression. TCS 364(3), 273\u2013291 (2006). https:\/\/doi.org\/10.1016\/j.tcs.2006.08.012","journal-title":"TCS"},{"key":"9_CR46","doi-asserted-by":"publisher","unstructured":"Johannsen, C., Nukala, K., Dureja, R., Irfan, A., Shankar, N., Tinelli, C., Vardi, M.Y., Rozier, K.Y.: The MoXI model exchange tool suite. In: Proc. CAV. pp. 203\u2013218. LNCS\u00a014681, Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-65627-9_10","DOI":"10.1007\/978-3-031-65627-9_10"},{"key":"9_CR47","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":"9_CR48","unstructured":"Snyder, W.: Verilator. https:\/\/www.veripool.org\/verilator\/, accessed: 2023-01-29"},{"key":"9_CR49","doi-asserted-by":"publisher","unstructured":"Smrcka, A., Vojnar, T.: Verifying parametrised hardware designs via counter automata. In: Proc. HVC. pp. 51\u201368. LNCS\u00a04899, Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-77966-7_8","DOI":"10.1007\/978-3-540-77966-7_8"},{"key":"9_CR50","doi-asserted-by":"publisher","unstructured":"IEEE standard for VHDL language reference manual (2019). https:\/\/doi.org\/10.1109\/IEEESTD.2019.8938196","DOI":"10.1109\/IEEESTD.2019.8938196"},{"key":"9_CR51","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6","author":"KL McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Springer (1993). https:\/\/doi.org\/10.1007\/978-1-4615-3190-6","journal-title":"Symbolic Model Checking. Springer"},{"key":"9_CR52","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":"9_CR53","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":"9_CR54","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":"9_CR55","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":"9_CR56","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":"9_CR57","unstructured":"The CIRCT project: Circuit IR compilers and tools. https:\/\/circt.llvm.org\/, accessed: 2024-05-14"},{"key":"9_CR58","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":"9_CR59","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":"9_CR60","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":"9_CR61","doi-asserted-by":"publisher","unstructured":"Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: Cil: Intermediate language and tools for analysis and transformation of C programs. In: Proc. CC. pp. 213\u2013228. LNCS\u00a02304, Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45937-5_16","DOI":"10.1007\/3-540-45937-5_16"},{"key":"9_CR62","doi-asserted-by":"publisher","unstructured":"Falke, S., Merz, F., Sinz, C.: The bounded model checker Llbmc. In: Proc. ASE. pp. 706\u2013709. IEEE (2013). https:\/\/doi.org\/10.1109\/ASE.2013.6693138","DOI":"10.1109\/ASE.2013.6693138"},{"key":"9_CR63","doi-asserted-by":"publisher","unstructured":"Priya, S., Su, Y., Bao, Y., Zhou, X., Vizel, Y., Gurfinkel, A.: Bounded model checking for Llvm. In: Proc. FMCAD. pp. 214\u2013224. IEEE (2022). https:\/\/doi.org\/10.34727\/2022\/ISBN.978-3-85448-053-2_28","DOI":"10.34727\/2022\/ISBN.978-3-85448-053-2_28"},{"key":"9_CR64","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)"},{"key":"9_CR65","doi-asserted-by":"publisher","unstructured":"Slab\u00fd, J., Strej\u010dek, J., Trt\u00edk, M.: Checking properties described by state machines: On synergy of instrumentation, slicing, and symbolic execution. In: Proc. FMICS. pp. 207\u2013221. LNCS\u00a07437, Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-32469-7_14","DOI":"10.1007\/978-3-642-32469-7_14"},{"key":"9_CR66","doi-asserted-by":"publisher","unstructured":"Jon\u00e1\u0161, M., Kumor, K., Nov\u00e1k, J., Sedl\u00e1\u010dek, J., Trt\u00edk, M., Zaoral, L., Ayaziov\u00e1, P., Strej\u010dek, J.: Symbiotic 10: Lazy memory initialization and compact symbolic execution (competition contribution). In: Proc. TACAS\u00a0(3). pp. 406\u2013411. LNCS\u00a014572, Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_29","DOI":"10.1007\/978-3-031-57256-2_29"},{"key":"9_CR67","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":"9_CR68","unstructured":"DeLine, R., Leino, R.: BoogiePL: A typed procedural language for checking object-oriented programs. Tech. Rep. MSR-TR-2005-70, Microsoft Research (2005)"},{"key":"9_CR69","doi-asserted-by":"publisher","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: Proc. FMCO. pp. 115\u2013137. LNCS\u00a04111, Springer (2005). https:\/\/doi.org\/10.1007\/11804192_6","DOI":"10.1007\/11804192_6"},{"key":"9_CR70","doi-asserted-by":"publisher","unstructured":"Bj\u00f8rner, N.S., McMillan, K.L., Rybalchenko, A.: Program verification as satisfiability modulo theories. In: Proc. SMT. EPiC Series in Computing, vol.\u00a020, pp. 3\u201311. EasyChair (2012). https:\/\/doi.org\/10.29007\/1l7f","DOI":"10.29007\/1l7f"},{"key":"9_CR71","doi-asserted-by":"publisher","unstructured":"Johnson, D.S., Trick, M.A. (eds.): Cliques, Coloring, and Satisfiability, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol.\u00a026. DIMACS\/AMS (1996). https:\/\/doi.org\/10.1090\/DIMACS\/026","DOI":"10.1090\/DIMACS\/026"},{"key":"9_CR72","doi-asserted-by":"publisher","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S., Clarke, E.M.: Automatic abstraction in SMT-based unbounded software model checking. In: Proc. CAV. pp. 846\u2013862. LNCS\u00a08044, Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_59","DOI":"10.1007\/978-3-642-39799-8_59"},{"key":"9_CR73","doi-asserted-by":"publisher","unstructured":"Fedyukovich, G., Prabhu, S., Madhukar, K., Gupta, A.: Solving constrained Horn clauses using syntax and data. In: Proc. FMCAD. pp.\u00a01\u20139. IEEE (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8603011","DOI":"10.23919\/FMCAD.2018.8603011"},{"key":"9_CR74","doi-asserted-by":"publisher","unstructured":"Hojjat, H., R\u00fcmmer, P.: The ELDARICA Horn solver. In: Proc. FMCAD. pp.\u00a01\u20137. IEEE (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8603013","DOI":"10.23919\/FMCAD.2018.8603013"},{"key":"9_CR75","doi-asserted-by":"publisher","unstructured":"Blicha, M., Britikov, K., Sharygina, N.: The Golem Horn solver. In: Proc. CAV. pp. 209\u2013223. LNCS\u00a013965, Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_10","DOI":"10.1007\/978-3-031-37703-7_10"},{"key":"9_CR76","unstructured":"Kroening, D., Purandare, M.: EBMC. http:\/\/www.cprover.org\/ebmc\/, accessed: 2023-01-29"},{"key":"9_CR77","doi-asserted-by":"publisher","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Viper: A verification infrastructure for permission-based reasoning. In: Proc. VMCAI. pp. 41\u201362. LNCS\u00a09583, Springer (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_2","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"9_CR78","doi-asserted-by":"publisher","unstructured":"Dellacherie, S., Devulder, S., Lambert, J.L.: Software verification based on linear programming. In: Proc. FM. pp. 1147\u20131165. LNCS\u00a01709, Springer (1999). https:\/\/doi.org\/10.1007\/3-540-48118-4_11","DOI":"10.1007\/3-540-48118-4_11"},{"key":"9_CR79","doi-asserted-by":"publisher","unstructured":"Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: Proc. CAV. pp. 3\u201329. LNCS\u00a010426, Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_1","DOI":"10.1007\/978-3-319-63387-9_1"},{"key":"9_CR80","doi-asserted-by":"publisher","unstructured":"Zhang, Y., Zhao, Z., Chen, G., Song, F., Zhang, M., Chen, T., Sun, J.: QVIP: An ILP-based formal verification approach for quantized neural networks. In: Proc. ASE. pp. 82:1\u201382:13. ACM (2022). https:\/\/doi.org\/10.1145\/3551349.3556916","DOI":"10.1145\/3551349.3556916"},{"key":"9_CR81","doi-asserted-by":"publisher","unstructured":"Necula, G.C., McPeak, S., Weimer, W.: CCured: Type-safe retrofitting of legacy code. In: Proc. POPL. pp. 128\u2013139. ACM (2002). https:\/\/doi.org\/10.1145\/503272.503286","DOI":"10.1145\/503272.503286"},{"key":"9_CR82","doi-asserted-by":"publisher","unstructured":"Amilon, J., Esen, Z., Gurov, D., Lidstr\u00f6m, C., R\u00fcmmer, P.: Automatic program instrumentation for automatic verification. In: Proc. CAV. pp. 281\u2013304. LNCS\u00a013966, Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37709-9_14","DOI":"10.1007\/978-3-031-37709-9_14"},{"key":"9_CR83","doi-asserted-by":"publisher","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proc. LICS. pp. 55\u201374. IEEE Computer Society (2002). https:\/\/doi.org\/10.1109\/LICS.2002.1029817","DOI":"10.1109\/LICS.2002.1029817"},{"issue":"1","key":"9_CR84","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1109\/TSE.2004.1265732","volume":"30","author":"M Harman","year":"2004","unstructured":"Harman, M., Hu, L., Hierons, R.M., Wegener, J., Sthamer, H., Baresel, A., Roper, M.: Testability transformation. IEEE Trans. Softw. Eng. 30(1), 3\u201316 (2004). https:\/\/doi.org\/10.1109\/TSE.2004.1265732","journal-title":"IEEE Trans. Softw. Eng."},{"key":"9_CR85","doi-asserted-by":"publisher","unstructured":"Apel, S., Beyer, D., Mordan, V.O., Mutilin, V.S., Stahlbauer, A.: On-the-fly decomposition of specifications in software model checking. In: Proc. FSE. pp. 349\u2013361. ACM (2016). https:\/\/doi.org\/10.1145\/2950290.2950349","DOI":"10.1145\/2950290.2950349"},{"key":"9_CR86","doi-asserted-by":"publisher","unstructured":"Beyer, D., Chlipala, A.J., Henzinger, T.A., Jhala, R., Majumdar, R.: Generating tests from counterexamples. In: Proc. ICSE. pp. 326\u2013335. IEEE (2004). https:\/\/doi.org\/10.1109\/ICSE.2004.1317455","DOI":"10.1109\/ICSE.2004.1317455"},{"issue":"4","key":"9_CR87","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1109\/tse.1984.5010248","volume":"10","author":"M Weiser","year":"1984","unstructured":"Weiser, M.: Program slicing. IEEE Trans. Softw. Eng. 10(4), 352\u2013357 (1984). https:\/\/doi.org\/10.1109\/tse.1984.5010248","journal-title":"IEEE Trans. Softw. Eng."},{"key":"9_CR88","doi-asserted-by":"publisher","unstructured":"Chalupa, M., Strej\u010dek, J.: Evaluation of program slicing in software verification. In: Proc. IFM. pp. 101\u2013119. LNCS\u00a011918, Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-34968-4_6","DOI":"10.1007\/978-3-030-34968-4_6"},{"key":"9_CR89","doi-asserted-by":"publisher","unstructured":"Westhofen, L., Berger, P., Katoen, J.P.: Benchmarking software model checkers on automotive code. In: Proc. NFM. pp. 133\u2013150. LNCS\u00a012229, Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-55754-6_8","DOI":"10.1007\/978-3-030-55754-6_8"},{"key":"9_CR90","unstructured":"Berger, P.: Applying Software Model Checking: Experiences and Advancements. Ph.D. thesis, RWTH Aachen (2023)"},{"key":"9_CR91","doi-asserted-by":"publisher","unstructured":"Lifschitz, V., Turner, H.: Splitting a logic program. In: Proc. ICLP. pp. 23\u201337. MIT Press (1994). https:\/\/doi.org\/10.7551\/mitpress\/4316.003.0014","DOI":"10.7551\/mitpress\/4316.003.0014"},{"key":"9_CR92","doi-asserted-by":"publisher","unstructured":"Siddiqui, J.H., Khurshid, S.: Scaling symbolic execution using ranged analysis. In: Leavens, G.T., Dwyer, M.B. (eds.) Proc. SPLASH. pp. 523\u2013536. ACM (2012). https:\/\/doi.org\/10.1145\/2384616.2384654","DOI":"10.1145\/2384616.2384654"},{"key":"9_CR93","doi-asserted-by":"publisher","unstructured":"Haltermann, J., Jakobs, M.C., Richter, C., Wehrheim, H.: Parallel program analysis via range splitting. In: Proc. FASE. pp. 195\u2013219 (2023). https:\/\/doi.org\/10.1007\/978-3-031-30826-0_11","DOI":"10.1007\/978-3-031-30826-0_11"},{"key":"9_CR94","doi-asserted-by":"publisher","unstructured":"Sherman, E., Dwyer, M.B.: Structurally defined conditional data-flow static analysis. In: Proc. TACAS\u00a0(2). pp. 249\u2013265. LNCS\u00a010806, Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_15","DOI":"10.1007\/978-3-319-89963-3_15"},{"key":"9_CR95","doi-asserted-by":"publisher","unstructured":"Beyer, D., Friedberger, K.: Domain-independent multi-threaded software model checking. In: Proc. ASE. pp. 634\u2013644. ACM (2018). https:\/\/doi.org\/10.1145\/3238147.3238195","DOI":"10.1145\/3238147.3238195"},{"key":"9_CR96","doi-asserted-by":"publisher","unstructured":"Zhou, L.: Foundationally sound annotation verifier via control flow splitting. In: Proc. SPLASH. pp. 69\u201371. ACM (2022). https:\/\/doi.org\/10.1145\/3563768.3563956","DOI":"10.1145\/3563768.3563956"},{"key":"9_CR97","doi-asserted-by":"publisher","unstructured":"Chalupa, M., Richter, C.: Bubaak-SpLit: Split what you cannot verify (competition contribution). In: Proc. TACAS\u00a0(3). pp. 353\u2013358. LNCS\u00a014572, Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_20","DOI":"10.1007\/978-3-031-57256-2_20"},{"key":"9_CR98","doi-asserted-by":"publisher","unstructured":"Lerner, S., Grove, D., Chambers, C.: Composing data-flow analyses and transformations. In: Proc. POPL. pp. 270\u2013282. ACM (2002). https:\/\/doi.org\/10.1145\/503272.503298","DOI":"10.1145\/503272.503298"},{"key":"9_CR99","doi-asserted-by":"publisher","unstructured":"Beyer, D., Henzinger, T.A., Keremoglu, M.E., Wendler, P.: Conditional model checking: A technique to pass information between verifiers. In: Proc. FSE. ACM (2012). https:\/\/doi.org\/10.1145\/2393596.2393664","DOI":"10.1145\/2393596.2393664"},{"key":"9_CR100","doi-asserted-by":"publisher","unstructured":"Christakis, M., M\u00fcller, P., W\u00fcstholz, V.: Collaborative verification and testing with explicit assumptions. In: Proc. FM. pp. 132\u2013146. LNCS\u00a07436, Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-32759-9_13","DOI":"10.1007\/978-3-642-32759-9_13"},{"key":"9_CR101","doi-asserted-by":"publisher","unstructured":"Christakis, M., M\u00fcller, P., W\u00fcstholz, V.: Guiding dynamic symbolic execution toward unverified program executions. In: Proc. ICSE. pp. 144\u2013155. ACM (2016). https:\/\/doi.org\/10.1145\/2884781.2884843","DOI":"10.1145\/2884781.2884843"},{"key":"9_CR102","doi-asserted-by":"publisher","unstructured":"Shankar, N.: Combining model checking and deduction. In: Handbook of Model Checking., pp. 651\u2013684. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_20","DOI":"10.1007\/978-3-319-10575-8_20"},{"key":"9_CR103","unstructured":"Boigelot, B.: Symbolic Methods for Exploring Infinite State Spaces. Ph.D. thesis, Facult\u00e9 des Sciences Appliqu\u00e9es de Universit\u00e9 de Li\u00e8ge (1998)"},{"key":"9_CR104","doi-asserted-by":"publisher","unstructured":"Bardin, S., Finkel, A., Leroux, J., Schnoebelen, P.: Flat acceleration in symbolic model checking. In: Proc. ATVA. pp. 474\u2013488. LNCS\u00a03707, Springer (2005). https:\/\/doi.org\/10.1007\/11562948_35","DOI":"10.1007\/11562948_35"},{"key":"9_CR105","doi-asserted-by":"publisher","unstructured":"Kumar, S., Sanyal, A., Venkatesh, R., Shah, P.: Property checking array programs using loop shrinking. In: Proc. TACAS\u00a0(1). pp. 213\u2013231. LNCS\u00a010805, Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_12","DOI":"10.1007\/978-3-319-89960-2_12"},{"key":"9_CR106","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. IEEE (2019). https:\/\/doi.org\/10.1109\/ASE.2019.00121","DOI":"10.1109\/ASE.2019.00121"},{"key":"9_CR107","doi-asserted-by":"publisher","unstructured":"Beyer, D., Lingsch-Rosenfeld, M., Spiessl, M.: A unifying approach for control-flow-based loop abstraction. In: Proc. SEFM. pp. 3\u201319. LNCS\u00a013550, Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-17108-6_1","DOI":"10.1007\/978-3-031-17108-6_1"},{"key":"9_CR108","doi-asserted-by":"publisher","unstructured":"Beyer, D., Lingsch-Rosenfeld, M., Spiessl, M.: CEGAR-PT: A tool for abstraction by program transformation. In: Proc. ASE. pp. 2078\u20132081. IEEE (2023). https:\/\/doi.org\/10.1109\/ASE56229.2023.00215","DOI":"10.1109\/ASE56229.2023.00215"},{"key":"9_CR109","doi-asserted-by":"publisher","unstructured":"Chalupa, M., Strej\u010dek, J., Vitovsk\u00e1, M.: Joint forces for memory safety checking. In: Proc. SPIN. pp. 115\u2013132. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-94111-0_7","DOI":"10.1007\/978-3-319-94111-0_7"},{"key":"9_CR110","doi-asserted-by":"publisher","unstructured":"Beyer, D., Kanav, S., Richter, C.: Construction of verifier combinations based on off-the-shelf verifiers. In: Proc. FASE. pp. 49\u201370. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99429-7_3","DOI":"10.1007\/978-3-030-99429-7_3"},{"issue":"3","key":"9_CR111","doi-asserted-by":"publisher","first-page":"695","DOI":"10.1007\/S10270-024-01155-3","volume":"23","author":"J Haltermann","year":"2024","unstructured":"Haltermann, J., Wehrheim, H.: Exchanging information in cooperative software validation. Softw. Syst. Model. 23(3), 695\u2013719 (2024). https:\/\/doi.org\/10.1007\/S10270-024-01155-3","journal-title":"Softw. Syst. Model."},{"key":"9_CR112","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":"9_CR113","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":"9_CR114","unstructured":"Biere, A., Froleyks, N., Preiner, M.: 11th hardware model-checking competition (HWMCC 2020). http:\/\/fmv.jku.at\/hwmcc20\/, accessed: 2023-01-29"},{"key":"9_CR115","doi-asserted-by":"publisher","unstructured":"Beyer, D.: State of the art in software verification and witness validation: SV-COMP 2024. In: Proc. TACAS\u00a0(3). pp. 299\u2013329. LNCS\u00a014572, Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_15","DOI":"10.1007\/978-3-031-57256-2_15"},{"key":"9_CR116","unstructured":"Long, J.: Reasoning about High-Level Constructs in Hardware\/Software Formal Verification. Ph.D. thesis, EECS Department, University of California, Berkeley (2017), http:\/\/www2.eecs.berkeley.edu\/Pubs\/TechRpts\/2017\/EECS-2017-150.html"},{"key":"9_CR117","doi-asserted-by":"publisher","unstructured":"Griggio, A., Jon\u00e1\u0161, M.: Kratos2: An SMT-based model checker for imperative programs. In: Proc. CAV. pp. 423\u2013436. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37709-9_20","DOI":"10.1007\/978-3-031-37709-9_20"},{"key":"9_CR118","unstructured":"Cimatti, A., Griggio, A., Tonetta, S.: The VMT-LIB language and tools. In: Proc. SMT. CEUR Workshop Proceedings, vol.\u00a03185, pp. 80\u201389. CEUR-WS.org (2022)"},{"key":"9_CR119","doi-asserted-by":"crossref","unstructured":"Rozier, K.Y., Dureja, R., Irfan, A., Johannsen, C., Nukala, K., Shankar, N., Tinelli, C., Vardi, M.Y.: MoXI: An intermediate language for symbolic model checking. In: Proc. SPIN. LNCS\u00a0, Springer (2024)","DOI":"10.1007\/978-3-031-66149-5_2"},{"key":"9_CR120","doi-asserted-by":"publisher","unstructured":"Beyer, D., Chien, P.C., Lee, N.Z.: MoXIchecker: An extensible model checker for MoXI. arXiv\/CoRR 2407(15551) (July 2024). https:\/\/doi.org\/10.48550\/arXiv.2407.15551","DOI":"10.48550\/arXiv.2407.15551"},{"key":"9_CR121","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":"9_CR122","unstructured":"Baudin, P., Cuoq, P., Filli\u00e2tre, J.C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI\/ISO C specification language version 1.17 (2021), available at https:\/\/frama-c.com\/download\/acsl-1.17.pdf"},{"key":"9_CR123","doi-asserted-by":"publisher","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C. In: Proc. SEFM. pp. 233\u2013247. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-33826-7_16","DOI":"10.1007\/978-3-642-33826-7_16"},{"key":"9_CR124","unstructured":"Beyer, D.: Conservation and accessibility of tools for formal methods. In: Proc. Festschrift Podelski 65th Birthday. Springer (2024)"},{"key":"9_CR125","unstructured":"Beyer, D.: Tools for formal methods. https:\/\/fm-tools.sosy-lab.org\/, accessed: 2024-08-21"},{"key":"9_CR126","doi-asserted-by":"publisher","unstructured":"Beyer, D., Jakobs, M.C.: CoVeriTest: Cooperative verifier-based testing. In: Proc. FASE. pp. 389\u2013408. LNCS\u00a011424, Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-16722-6_23","DOI":"10.1007\/978-3-030-16722-6_23"},{"key":"9_CR127","doi-asserted-by":"publisher","unstructured":"Jakobs, M.C., Richter, C.: CoVeriTest with adaptive time scheduling (competition contribution). In: Proc. FASE. pp. 358\u2013362. LNCS\u00a012649, Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-71500-7_18","DOI":"10.1007\/978-3-030-71500-7_18"},{"key":"9_CR128","doi-asserted-by":"publisher","unstructured":"Fischer, B., Inverso, O., Parlato, G.: CSeq: A concurrency pre-processor for sequential C verification tools. In: Proc. ASE. pp. 710\u2013713. IEEE (2013). https:\/\/doi.org\/10.1109\/ASE.2013.6693139","DOI":"10.1109\/ASE.2013.6693139"},{"key":"9_CR129","doi-asserted-by":"publisher","unstructured":"Czech, M., Jakobs, M., Wehrheim, H.: Just test what you cannot verify! In: Proc. FASE. pp. 100\u2013114. LNCS\u00a09033, Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46675-9_7","DOI":"10.1007\/978-3-662-46675-9_7"},{"key":"9_CR130","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":"9_CR131","doi-asserted-by":"publisher","unstructured":"Ball, T., Rajamani, S.K.: Bebop: A symbolic model checker for Boolean programs. In: Proc. SPIN. pp. 113\u2013130. LNCS\u00a01885, Springer (2000). https:\/\/doi.org\/10.1007\/10722468_7","DOI":"10.1007\/10722468_7"},{"issue":"5\u20136","key":"9_CR132","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker Blast. Int. J. Softw. Tools Technol. Transfer 9(5\u20136), 505\u2013525 (2007). https:\/\/doi.org\/10.1007\/s10009-007-0044-z","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"9_CR133","doi-asserted-by":"publisher","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Terminator: Beyond safety. In: Proc. CAV. pp. 415\u2013418. LNCS\u00a04144, Springer (2006). https:\/\/doi.org\/10.1007\/11817963_37","DOI":"10.1007\/11817963_37"},{"key":"9_CR134","doi-asserted-by":"publisher","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: Proc. PLDI. pp. 415\u2013426. ACM (2006). https:\/\/doi.org\/10.1145\/1133981.1134029","DOI":"10.1145\/1133981.1134029"},{"key":"9_CR135","doi-asserted-by":"publisher","unstructured":"Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Proc. VMCAI. pp. 239\u2013251. LNCS\u00a02937, Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-24622-0_20","DOI":"10.1007\/978-3-540-24622-0_20"},{"issue":"5","key":"9_CR136","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"EM Clarke","year":"2003","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","journal-title":"J. ACM"},{"issue":"2","key":"9_CR137","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/S10009-019-00547-X","volume":"22","author":"T Lange","year":"2020","unstructured":"Lange, T., Neuh\u00e4u\u00dfer, M.R., Noll, T., Katoen, J.P.: IC3 software model checking. Int. J. Softw. Tools Technol. Transf. 22(2), 135\u2013161 (2020). https:\/\/doi.org\/10.1007\/S10009-019-00547-X","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"9_CR138","unstructured":"Beyer, D., Lee, N.Z., Wendler, P.: Interpolation and SAT-based model checking revisited: Adoption to software verification. J. Autom. Reasoning (2024) 10.1007\/s10817-024-09702-9, preprint: https:\/\/doi.org\/10.48550\/arXiv.2208.05046"},{"key":"9_CR139","doi-asserted-by":"publisher","unstructured":"Beyer, D., Chien, P.C., Jankola, M., Lee, N.Z.: A transferability study of interpolation-based hardware model checking for software verification. Proc. ACM Softw. Eng. 1(FSE) (2024). https:\/\/doi.org\/10.1145\/3660797","DOI":"10.1145\/3660797"},{"key":"9_CR140","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":"9_CR141","doi-asserted-by":"crossref","unstructured":"Ayaziov\u00e1, P., Beyer, D., Lingsch-Rosenfeld, M., Spiessl, M., Strej\u010dek, J.: Software verification witnesses\u00a02.0. In: Proc. SPIN. Springer (2024)","DOI":"10.1007\/978-3-031-66149-5_11"},{"key":"9_CR142","unstructured":"Heule, M.J.H.: The DRAT format and drat-trim checker. CoRR 1610(06229) (October 2016)"},{"key":"9_CR143","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M.: Verification-aided debugging: An interactive web-service for exploring error witnesses. In: Proc. CAV\u00a0(2). pp. 502\u2013509. LNCS\u00a09780, Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_28","DOI":"10.1007\/978-3-319-41540-6_28"},{"key":"9_CR144","doi-asserted-by":"publisher","unstructured":"Haltermann, J., Wehrheim, H.: CoVEGI: Cooperative verification via externally generated invariants. In: Proc. FASE. pp. 108\u2013129. LNCS\u00a012649 (2021). https:\/\/doi.org\/10.1007\/978-3-030-71500-7_6","DOI":"10.1007\/978-3-030-71500-7_6"}],"container-title":["Lecture Notes in Computer Science","Principles of Verification: Cycling the Probabilistic Landscape"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-75778-5_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,17]],"date-time":"2024-11-17T13:03:44Z","timestamp":1731848624000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-75778-5_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,18]]},"ISBN":["9783031757778","9783031757785"],"references-count":144,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-75778-5_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,11,18]]},"assertion":[{"value":"18 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}