{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,29]],"date-time":"2026-01-29T22:56:49Z","timestamp":1769727409398,"version":"3.49.0"},"publisher-location":"Cham","reference-count":86,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032068460","type":"print"},{"value":"9783032068477","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T00:00:00Z","timestamp":1761955200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T00:00:00Z","timestamp":1761955200000},"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":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Software verification is a complex problem, and verification tools need significant tuning to achieve high performance. Due to this, many verifiers choose to specialize on basic reachability properties. Instead of implementing algorithms for each possible specification, some verifiers implement known transformations from the given specification to reachability on their internal representations. Unfortunately, those internal transformations are not reusable by others. To improve this situation, we propose\u00a0\n                    <jats:sc>TransVer<\/jats:sc>\n                    , a tool which offers transformations as modular stand-alone component, modifying the input program instead of the internal representation, enabling their usage as a preprocessing step by other verifiers. This way, we separate two concerns: improving the performance of reachability analyses\u00a0and implementing efficient transformations of arbitrary specifications to reachability. We implement the transformations in a framework that is based on\n                    <jats:italic>instrumentation automata<\/jats:italic>\n                    , inspired by the BLAST query language. In our initial study, we support three important concrete specifications for C\u00a0programs:\n                    <jats:italic>termination<\/jats:italic>\n                    ,\n                    <jats:italic>no-overflow<\/jats:italic>\n                    , and\n                    <jats:italic>memory cleanup<\/jats:italic>\n                    . We conduct experiments with ten different verifiers. The experiments evaluate the efficiency and effectiveness of our transformations. The results are promising: Our transformations can extend existing verifiers to be effective on specifications for which they have no integrated support, and the efficiency is often similar or better\u00a0to state-of-the-art verifiers that have integrated support for\u00a0the considered specifications.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-06847-7_1","type":"book-chapter","created":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T23:42:25Z","timestamp":1761954145000},"page":"1-24","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["TransVer: A Modular Program-Transformation Framework for Reduction to Reachability"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4832-7662","authenticated-orcid":false,"given":"Dirk","family":"Beyer","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0008-7961-190X","authenticated-orcid":false,"given":"Marek","family":"Jankola","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8172-3184","authenticated-orcid":false,"given":"Marian","family":"Lingsch-Rosenfeld","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0006-4767-8435","authenticated-orcid":false,"given":"Tian","family":"Xia","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0007-7298-6998","authenticated-orcid":false,"given":"Xiyue","family":"Zheng","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,11,1]]},"reference":[{"key":"1_CR1","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":"1_CR2","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":"1_CR3","doi-asserted-by":"publisher","unstructured":"Baier, D., Beyer, D., Chien, P.C., Jakobs, M.C., Jankola, M., Kettl, M., Lee, N.Z., Lemberger, T., Lingsch-Rosenfeld, M., Wachowitz, H., Wendler, P.: Software verification with CPAchecker 3.0: Tutorial and user guide. In: Proc. FM. pp. 543\u2013570. LNCS\u00a014934, Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-71177-0_30","DOI":"10.1007\/978-3-031-71177-0_30"},{"key":"1_CR4","doi-asserted-by":"publisher","unstructured":"Beyer, D., Chlipala, A.J., Henzinger, T.A., Jhala, R., Majumdar, R.: The Blast query language for software verification. In: Proc. SAS. pp. 2\u201318. LNCS\u00a03148, Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-27864-1_2","DOI":"10.1007\/978-3-540-27864-1_2"},{"key":"1_CR5","unstructured":"Ball, T., Rajamani, S.K.: SLIC: A specification language for interface checking (of\u00a0C). Tech. Rep. MSR-TR-2001-21, Microsoft Research (2002)"},{"key":"1_CR6","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":"1_CR7","doi-asserted-by":"publisher","unstructured":"O. \u015cer\u00fd: Enhanced property specification and verification in Blast. In: Proc. FASE. pp. 456\u2013469. LNCS\u00a05503, Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-00593-0_32","DOI":"10.1007\/978-3-642-00593-0_32"},{"key":"1_CR8","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":"1_CR9","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":"1_CR10","doi-asserted-by":"publisher","unstructured":"Metta, R., Medicherla, R.K., Karmarkar, H.: VeriFuzz: Fuzz centric test generation tool (competition contribution). In: Proc. FASE. pp. 341\u2013346. LNCS\u00a013241, Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99429-7_20","DOI":"10.1007\/978-3-030-99429-7_20"},{"key":"1_CR11","doi-asserted-by":"publisher","unstructured":"Metta, R., Medicherla, R.K., Chakraborty, S.: BMC+Fuzz: Efficient and effective test generation. In: Proc. DATE. pp. 1419\u20131424. IEEE (2022). https:\/\/doi.org\/10.23919\/DATE54114.2022.9774672","DOI":"10.23919\/DATE54114.2022.9774672"},{"key":"1_CR12","doi-asserted-by":"publisher","unstructured":"Bajczi, L., Szekeres, D., Mondok, M., \u00c1d\u00e1m, Z., Somorjai, M., Telbisz, C., Dobos-Kov\u00e1cs, M., Moln\u00e1r, V.: EmergenTheta: Verification beyond abstraction refinement (competition contribution). In: Proc. TACAS\u00a0(3). pp. 371\u2013375. LNCS\u00a014572, Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_23","DOI":"10.1007\/978-3-031-57256-2_23"},{"key":"1_CR13","doi-asserted-by":"publisher","unstructured":"Bajczi, L., Telbisz, C., Somorjai, M., \u00c1d\u00e1m, Z., Dobos-Kov\u00e1cs, M., Szekeres, D., Mondok, M., Moln\u00e1r, V.: Theta: Abstraction based techniques for verifying concurrency (competition contribution). In: Proc. TACAS\u00a0(3). pp. 412\u2013417. LNCS\u00a014572, Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_30","DOI":"10.1007\/978-3-031-57256-2_30"},{"key":"1_CR14","doi-asserted-by":"publisher","unstructured":"Beyer, D., Jankola, M., Lingsch-Rosenfeld, M., Xia, T., Zheng, X.: A modular program-transformation framework for reducing specifications to reachability. arXiv\/CoRR 2501(16310) (January 2025). https:\/\/doi.org\/10.48550\/arXiv.2501.16310","DOI":"10.48550\/arXiv.2501.16310"},{"key":"1_CR15","doi-asserted-by":"publisher","unstructured":"Partsch, H., Steinbr\u00fcggen, R.: Program transformation systems. ACM Comput. Surv. 15(3), 199\u2013236 (1983). https:\/\/doi.org\/10.1145\/356914.356917","DOI":"10.1145\/356914.356917"},{"key":"1_CR16","doi-asserted-by":"publisher","unstructured":"Visser, E.: A survey of strategies in program-transformation systems. In: Proc. WRS. pp. 109\u2013143. ENTCS\u00a057, Elsevier (2001). https:\/\/doi.org\/10.1016\/S1571-0661(04)00270-1","DOI":"10.1016\/S1571-0661(04)00270-1"},{"key":"1_CR17","doi-asserted-by":"publisher","unstructured":"Beyer, D., Lee, N.Z.: The transformation game: Joining forces for verification. In: Principles of Verification: Cycling the Probabilistic Landscape. pp. 175\u2013205. LNCS\u00a015262, Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-75778-5_9","DOI":"10.1007\/978-3-031-75778-5_9"},{"key":"1_CR18","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":"1_CR19","doi-asserted-by":"publisher","unstructured":"Inverso, O., Nguyen, T.L., Fischer, B., La\u00a0Torre, S., Parlato, G.: Lazy-CSeq: A context-bounded model checking tool for multi-threaded C programs. In: Proc. ASE. pp. 807\u2013812. IEEE (2015). https:\/\/doi.org\/10.1109\/ASE.2015.108","DOI":"10.1109\/ASE.2015.108"},{"key":"1_CR20","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":"1_CR21","unstructured":"Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison-Wesley (1986)"},{"key":"1_CR22","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":"1_CR23","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":"1_CR24","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":"1_CR25","doi-asserted-by":"publisher","unstructured":"Jeannet, B., Schrammel, P., Sankaranarayanan, S.: Abstract acceleration of general linear loops. In: Proc. POPL. pp. 529\u2013540. ACM (2014). https:\/\/doi.org\/10.1145\/2535838.2535843","DOI":"10.1145\/2535838.2535843"},{"key":"1_CR26","doi-asserted-by":"publisher","unstructured":"Silverman, J., Kincaid, Z.: Loop summarization with rational vector addition systems. In: Proc. CAV, Part\u00a02. pp. 97\u2013115. LNCS\u00a011562, Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_7","DOI":"10.1007\/978-3-030-25543-5_7"},{"key":"1_CR27","doi-asserted-by":"publisher","unstructured":"Frohn, F.: A calculus for modular loop acceleration. In: Proc. TACAS (1). pp. 58\u201376. LNCS\u00a012078, Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_4","DOI":"10.1007\/978-3-030-45190-5_4"},{"key":"1_CR28","doi-asserted-by":"publisher","unstructured":"Madhukar, K., Wachter, B., Kr\u00f6ning, D., Lewis, M., Srivas, M.K.: Accelerating invariant generation. In: Proc. FMCAD. pp. 105\u2013111. IEEE (2015). https:\/\/doi.org\/10.1109\/FMCAD.2015.7542259","DOI":"10.1109\/FMCAD.2015.7542259"},{"key":"1_CR29","doi-asserted-by":"publisher","unstructured":"Bodden, E., Hendren, L.: The Clara framework for hybrid typestate analysis. Softw. Tools Technol. Transf. 14(3), 307\u2013326 (2012). https:\/\/doi.org\/10.1007\/s10009-010-0183-5","DOI":"10.1007\/s10009-010-0183-5"},{"key":"1_CR30","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"},{"key":"1_CR31","doi-asserted-by":"publisher","unstructured":"Zhang, Y., Xie, X., Li, Y., Chen, S., Zhang, C., Li, X.: EndWatch: A practical method for detecting non-termination in real-world software. In: Proc. ASE. pp. 686\u2013697 (2023). https:\/\/doi.org\/10.1109\/ASE56229.2023.00061","DOI":"10.1109\/ASE56229.2023.00061"},{"key":"1_CR32","doi-asserted-by":"publisher","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","DOI":"10.1016\/j.entcs.2005.11.018"},{"key":"1_CR33","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":"1_CR34","doi-asserted-by":"publisher","unstructured":"Robles, V., Kosmatov, N., Prevosto, V., Rilling, L., Le\u00a0Gall, P.: MetAcsl: Specification and verification of high-level properties. In: Proc. TACAS, Part\u00a01. pp. 358\u2013364. LNCS\u00a011427, Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_22","DOI":"10.1007\/978-3-030-17462-0_22"},{"key":"1_CR35","doi-asserted-by":"publisher","unstructured":"Robles, V., Kosmatov, N., Prevosto, V., Rilling, L., Gall, P.L.: Methodology for specification and verification of high-level requirements with MetAcsl. In: Proc. FormaliSE. pp. 54\u201367 (2021). https:\/\/doi.org\/10.1109\/FormaliSE52586.2021.00012","DOI":"10.1109\/FormaliSE52586.2021.00012"},{"key":"1_CR36","doi-asserted-by":"publisher","unstructured":"Blatter, L., Kosmatov, N., Le\u00a0Gall, P., Prevosto, V.: RPP: Automatic proof of relational properties by self-composition. In: Proc. TACAS. pp. 391\u2013397 (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_22","DOI":"10.1007\/978-3-662-54577-5_22"},{"key":"1_CR37","doi-asserted-by":"publisher","unstructured":"Blatter, L., Kosmatov, N., Le\u00a0Gall, P., Prevosto, V., Petiot, G.: Static and dynamic verification of relational properties on self-composed C code. In: Proc. TAP. pp. 44\u201362 (2018). https:\/\/doi.org\/10.1007\/978-3-319-92994-1_3","DOI":"10.1007\/978-3-319-92994-1_3"},{"key":"1_CR38","doi-asserted-by":"publisher","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","DOI":"10.1109\/TSE.2004.1265732"},{"key":"1_CR39","doi-asserted-by":"publisher","unstructured":"Harman, M.: We need a testability transformation semantics. In: Proc. SEFM. pp. 3\u201317. LNCS\u00a010886, Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-92970-5_1","DOI":"10.1007\/978-3-319-92970-5_1"},{"key":"1_CR40","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":"1_CR41","doi-asserted-by":"publisher","unstructured":"Ayaziov\u00e1, P., Beyer, D., Lingsch-Rosenfeld, M., Spiessl, M., Strej\u010dek, J.: Software verification witnesses\u00a02.0. In: Proc. SPIN. pp. 184\u2013203. LNCS\u00a014624, Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-66149-5_11","DOI":"10.1007\/978-3-031-66149-5_11"},{"key":"1_CR42","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":"1_CR43","doi-asserted-by":"publisher","unstructured":"Necula, G.C.: Proof-carrying code. In: Proc. POPL. pp. 106\u2013119. ACM (1997). https:\/\/doi.org\/10.1145\/263699.263712","DOI":"10.1145\/263699.263712"},{"key":"1_CR44","unstructured":"Julien, S.: E-ACSL: Executable ANSI\/ISO C specification language (2022), available at http:\/\/frama-c.com\/download\/e-acsl\/e-acsl.pdf"},{"key":"1_CR45","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":"1_CR46","doi-asserted-by":"publisher","unstructured":"Condit, J., Harren, M., McPeak, S., Necula, G.C., Weimer, W.: CCured in the real world. In: Proc. PLDI. pp. 232\u2013244. ACM (2003). https:\/\/doi.org\/10.1145\/781131.781157","DOI":"10.1145\/781131.781157"},{"key":"1_CR47","doi-asserted-by":"publisher","unstructured":"Jakobsson, A., Kosmatov, N., Signoles, J.: Fast as a shadow, expressive as a tree: hybrid memory monitoring for C. In: Proc. SAC. pp. 1765\u20131772. ACM (2015). https:\/\/doi.org\/10.1145\/2695664.2695815","DOI":"10.1145\/2695664.2695815"},{"key":"1_CR48","doi-asserted-by":"publisher","unstructured":"Vorobyov, K., Signoles, J., Kosmatov, N.: Shadow state encoding for efficient monitoring of block-level properties. In: Proc. ISMM. pp. 47\u201358. ACM (2017). https:\/\/doi.org\/10.1145\/3092255.3092269","DOI":"10.1145\/3092255.3092269"},{"key":"1_CR49","doi-asserted-by":"publisher","unstructured":"Kiczales, G., Hilsdale, E., Hugunin, J., Kersten, M., Palm, J., Griswold, W.G.: An overview of AspectJ. In: Proc. ECOOP. pp. 327\u2013353. Springer (2001). https:\/\/doi.org\/10.1007\/3-540-45337-7_18","DOI":"10.1007\/3-540-45337-7_18"},{"key":"1_CR50","doi-asserted-by":"publisher","unstructured":"Mahrenholz, D., Spinczyk, O., Schr\u00f6der-Preikschat, W.: Program instrumentation for debugging and monitoring with AspectC++. In: Proc. ISIRC. pp. 249\u2013256 (2002). https:\/\/doi.org\/10.1109\/ISORC.2002.1003713","DOI":"10.1109\/ISORC.2002.1003713"},{"key":"1_CR51","doi-asserted-by":"publisher","unstructured":"Vitovsk\u00e1, M., Chalupa, M., Strej\u010dek, J.: SBT-Instrumentation: A tool for configurable instrumentation of LLVM bitcode. arXiv\/CoRR 1810(12617) (2018). https:\/\/doi.org\/10.48550\/arXiv.1810.12617","DOI":"10.48550\/arXiv.1810.12617"},{"key":"1_CR52","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":"1_CR53","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":"1_CR54","doi-asserted-by":"publisher","unstructured":"Menezes, R., Aldughaim, M., Farias, B., Li, X., Manino, E., Shmarov, F., Song, K., Brau\u00dfe, F., Gadelha, M.R., Tihanyi, N., Korovin, K., Cordeiro, L.: ESBMC v7.4: Harnessing the power of intervals (competition contribution). In: Proc. TACAS\u00a0(3). pp. 376\u2013380. LNCS\u00a014572, Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_24","DOI":"10.1007\/978-3-031-57256-2_24"},{"key":"1_CR55","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":"1_CR56","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 (2023). https:\/\/doi.org\/10.1007\/978-3-031-37709-9_14","DOI":"10.1007\/978-3-031-37709-9_14"},{"key":"1_CR57","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":"1_CR58","doi-asserted-by":"publisher","unstructured":"Piterman, N., Pnueli, A.: Temporal logic and fair discrete systems. In: Handbook of Model Checking, pp. 27\u201373. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_2","DOI":"10.1007\/978-3-319-10575-8_2"},{"key":"1_CR59","doi-asserted-by":"publisher","unstructured":"Beyer, D., Strej\u010dek, J.: Improvements in software verification and witness validation: SV-COMP 2025. In: Proc. TACAS\u00a0(3). pp. 151\u2013186. LNCS\u00a015698, Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-90660-2_9","DOI":"10.1007\/978-3-031-90660-2_9"},{"key":"1_CR60","unstructured":"American National Standards Institute: ANSI\/ISO\/IEC 9899-1999: Programming Languages \u2014 C. American National Standards Institute, 1430 Broadway, New York, NY 10018, USA (1999)"},{"key":"1_CR61","unstructured":"INT32-C. Ensure that operations on signed integers do not result in overflow. https:\/\/wiki.sei.cmu.edu\/confluence\/display\/c\/INT32-C.+Ensure+that+operations+on+signed+integers+do+not+result+in+overflow, [Accessed 2025-07-13]"},{"key":"1_CR62","doi-asserted-by":"publisher","unstructured":"Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. In: Proc. FMICS. pp. 160\u2013177. No.\u00a02 in ENTSC\u00a066, Elsevier (2002). https:\/\/doi.org\/10.1016\/S1571-0661(04)80410-9","DOI":"10.1016\/S1571-0661(04)80410-9"},{"key":"1_CR63","doi-asserted-by":"publisher","unstructured":"Beyer, D., Strej\u010dek, J.: SV-Benchmarks: Benchmark set for software verification (SV-COMP\u00a02025). Zenodo (2025). https:\/\/doi.org\/10.5281\/zenodo.15012096","DOI":"10.5281\/zenodo.15012096"},{"key":"1_CR64","doi-asserted-by":"publisher","unstructured":"Metta, R., Karmarkar, H., Madhukar, K., Venkatesh, R., Chakraborty, S.: Proton: Probes for non-termination and termination (competition contribution). In: Proc. TACAS\u00a0(3). pp. 393\u2013398. LNCS\u00a014572, Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_27","DOI":"10.1007\/978-3-031-57256-2_27"},{"key":"1_CR65","doi-asserted-by":"publisher","unstructured":"Darke, P., Chimdyalwar, B., Agrawal, S., Venkatesh, R., Chakraborty, S., Kumar, S.: VeriAbsL: Scalable verification by abstraction and strategy prediction (competition contribution). In: Proc. TACAS\u00a0(2). pp. 588\u2013593. LNCS\u00a013994, Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_41","DOI":"10.1007\/978-3-031-30820-8_41"},{"key":"1_CR66","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":"1_CR67","doi-asserted-by":"publisher","unstructured":"Mal\u00edk, V., Schrammel, P., Vojnar, T., Ne\u010das, F.: 2LS: Arrays and loop unwinding (competition contribution). In: Proc. TACAS\u00a0(2). pp. 529\u2013534. LNCS\u00a013994, Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_31","DOI":"10.1007\/978-3-031-30820-8_31"},{"key":"1_CR68","doi-asserted-by":"publisher","unstructured":"Viktor, M., Franti\u0161ek, N., Schrammel, P., Vojnar, T.: 2LS. Zenodo (2023). https:\/\/doi.org\/10.5281\/zenodo.10184626","DOI":"10.5281\/zenodo.10184626"},{"key":"1_CR69","doi-asserted-by":"publisher","unstructured":"Baier, D., Beyer, D., Chien, P.C., Jankola, M., Kettl, M., Lee, N.Z., Lemberger, T., Lingsch-Rosenfeld, M., Spiessl, M., Wachowitz, H., Wendler, P.: CPAchecker 2.3 with strategy selection (competition contribution). In: Proc. TACAS\u00a0(3). pp. 359\u2013364. LNCS\u00a014572, Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_21","DOI":"10.1007\/978-3-031-57256-2_21"},{"key":"1_CR70","doi-asserted-by":"publisher","unstructured":"Beyer, D., Wendler, P.: CPAchecker release 2.3 (unix). Zenodo (2023). https:\/\/doi.org\/10.5281\/zenodo.10203297","DOI":"10.5281\/zenodo.10203297"},{"key":"1_CR71","doi-asserted-by":"publisher","unstructured":"Vasilyev, A.: CPA-BAM-SMG (SV-COMP 2023). Zenodo (2022). https:\/\/doi.org\/10.5281\/zenodo.10396261","DOI":"10.5281\/zenodo.10396261"},{"key":"1_CR72","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"},{"key":"1_CR73","doi-asserted-by":"publisher","unstructured":"Chien, P.C., Lee, N.Z.: CPV release 0.6. Zenodo (2024). https:\/\/doi.org\/10.5281\/zenodo.14203582","DOI":"10.5281\/zenodo.14203582"},{"key":"1_CR74","doi-asserted-by":"publisher","unstructured":"Bajczi, L., Szekeres, D., Mondok, M., Moln\u00e1r, V.: EmergenTheta - SV-COMP\u201924 verifier archive. Zenodo (2023). https:\/\/doi.org\/10.5281\/zenodo.10198872","DOI":"10.5281\/zenodo.10198872"},{"key":"1_CR75","doi-asserted-by":"publisher","unstructured":"Peringer, P., \u0160okov\u00e1, V., Vojnar, T.: PredatorHP revamped (not only) for interval-sized memory regions and memory reallocation (competition contribution). In: Proc. TACAS\u00a0(2). pp. 408\u2013412. LNCS\u00a012079, Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-45237-7_30","DOI":"10.1007\/978-3-030-45237-7_30"},{"key":"1_CR76","doi-asserted-by":"publisher","unstructured":"\u0160okov\u00e1, V., Peringer, P., Vojnar, T., Kin\u0161t, O.: PredatorHP. Zenodo (2023). https:\/\/doi.org\/10.5281\/zenodo.10183805","DOI":"10.5281\/zenodo.10183805"},{"key":"1_CR77","doi-asserted-by":"publisher","unstructured":"Jon\u00e1\u0161, M., Kumor, K., Nov\u00e1k, J., Sedl\u00e1\u010dek, J., Shandilya, S., Trt\u00edk, M., Zaoral, L., Strej\u010dek, J.: Symbiotic 10: Submission to SV-COMP 2024. Zenodo (2023). https:\/\/doi.org\/10.5281\/zenodo.10202594","DOI":"10.5281\/zenodo.10202594"},{"key":"1_CR78","doi-asserted-by":"publisher","unstructured":"Bajczi, L., Szekeres, D., Mondok, M., Moln\u00e1r, V.: EmergenTheta - SV-COMP\u201924 verifier archive. Zenodo (2023). https:\/\/doi.org\/10.5281\/zenodo.10198872","DOI":"10.5281\/zenodo.10198872"},{"key":"1_CR79","doi-asserted-by":"publisher","unstructured":"Heizmann, M., Bentele, M., Dietsch, D., Jiang, X., Klumpp, D., Sch\u00fcssele, F., Podelski, A.: Ultimate Automizer and the abstraction of bitwise operations (competition contribution). In: Proc. TACAS\u00a0(3). pp. 418\u2013423. LNCS\u00a014572, Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_31","DOI":"10.1007\/978-3-031-57256-2_31"},{"key":"1_CR80","doi-asserted-by":"publisher","unstructured":"Dietsch, D., Bentele, M., Heizmann, M., Klumpp, D., Podelski, A., Sch\u00fcssele, F.: Ultimate Automizer SV-COMP 2024. Zenodo (2023). https:\/\/doi.org\/10.5281\/zenodo.10203545","DOI":"10.5281\/zenodo.10203545"},{"key":"1_CR81","doi-asserted-by":"publisher","unstructured":"Dietsch, D., Heizmann, M., Klumpp, D., Sch\u00fcssele, F., Podelski, A.: Ultimate Taipan 2023 (competition contribution). In: Proc. TACAS\u00a0(2). pp. 582\u2013587. LNCS\u00a013994, Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_40","DOI":"10.1007\/978-3-031-30820-8_40"},{"key":"1_CR82","doi-asserted-by":"publisher","unstructured":"Dietsch, D., Bentele, M., Heizmann, M., Klumpp, D., Podelski, A., Sch\u00fcssele, F.: Ultimate Taipan SV-COMP 2024. Zenodo (2023). https:\/\/doi.org\/10.5281\/zenodo.10203547","DOI":"10.5281\/zenodo.10203547"},{"key":"1_CR83","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":"1_CR84","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":"1_CR85","doi-asserted-by":"publisher","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Advances in Computers 58, 117\u2013148 (2003). https:\/\/doi.org\/10.1016\/S0065-2458(03)58003-2","DOI":"10.1016\/S0065-2458(03)58003-2"},{"key":"1_CR86","doi-asserted-by":"publisher","unstructured":"Beyer, D., Jankola, M., Lingsch-Rosenfeld, M., Xia, T., Zheng, X.: Reproduction package for SPIN\u00a02025 article \u2018TransVer: A modular program-transformation framework for reduction to reachability\u2019. Zenodo (2025). https:\/\/doi.org\/10.5281\/zenodo.15833440","DOI":"10.5281\/zenodo.15833440"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-06847-7_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T23:42:30Z","timestamp":1761954150000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-06847-7_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,1]]},"ISBN":["9783032068460","9783032068477"],"references-count":86,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-06847-7_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,1]]},"assertion":[{"value":"1 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SPIN","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Model Checking Software","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"spin2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/spin-web.github.io\/SPIN2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}