{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T20:55:10Z","timestamp":1777582510610,"version":"3.51.4"},"publisher-location":"Cham","reference-count":84,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031711763","type":"print"},{"value":"9783031711770","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T00:00:00Z","timestamp":1726185600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T00:00:00Z","timestamp":1726185600000},"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>This tutorial provides an introduction to<jats:sc>CPAchecker<\/jats:sc>for users.<jats:sc>CPAchecker<\/jats:sc>is a flexible and configurable framework for software verification and testing. The framework provides many abstract domains, such\u00a0as BDDs, explicit values, intervals, memory graphs,\u00a0and predicates, and many program-analysis and model-checking algorithms, such\u00a0as abstract interpretation, bounded model checking,<jats:sc>Impact<\/jats:sc>, interpolation-based model checking,<jats:italic>k<\/jats:italic>-induction, PDR, predicate abstraction,\u00a0and symbolic execution. This tutorial presents basic use cases for<jats:sc>CPAchecker<\/jats:sc>in formal software verification, focusing on its main verification techniques with their strengths and weaknesses. An extended version also shows further use cases of<jats:sc>CPAchecker<\/jats:sc>for test-case generation and witness-based result validation. The envisioned readers are assumed to possess a background in automatic formal verification and program analysis, but prior knowledge of<jats:sc>CPAchecker<\/jats:sc>is not required. This tutorial and user guide is based on<jats:sc>CPAchecker<\/jats:sc>in version\u00a03.0. This user guide\u2019s latest version and other documentation are available at<jats:ext-link xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" ext-link-type=\"uri\" xlink:href=\"https:\/\/cpachecker.sosy-lab.org\/doc.php\">https:\/\/cpachecker.sosy-lab.org\/doc.php<\/jats:ext-link>.<\/jats:p>","DOI":"10.1007\/978-3-031-71177-0_30","type":"book-chapter","created":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T06:10:51Z","timestamp":1726121451000},"page":"543-570","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Software Verification with CPAchecker 3.0: Tutorial and User Guide"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9116-1974","authenticated-orcid":false,"given":"Daniel","family":"Baier","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4832-7662","authenticated-orcid":false,"given":"Dirk","family":"Beyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5139-5178","authenticated-orcid":false,"given":"Po-Chun","family":"Chien","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5890-4673","authenticated-orcid":false,"given":"Marie-Christine","family":"Jakobs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-7961-190X","authenticated-orcid":false,"given":"Marek","family":"Jankola","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7365-5030","authenticated-orcid":false,"given":"Matthias","family":"Kettl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8096-5595","authenticated-orcid":false,"given":"Nian-Ze","family":"Lee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0291-815X","authenticated-orcid":false,"given":"Thomas","family":"Lemberger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8172-3184","authenticated-orcid":false,"given":"Marian","family":"Lingsch-Rosenfeld","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4768-4054","authenticated-orcid":false,"given":"Henrik","family":"Wachowitz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5139-341X","authenticated-orcid":false,"given":"Philipp","family":"Wendler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,9,13]]},"reference":[{"key":"30_CR1","unstructured":"Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison-Wesley (1986)"},{"key":"30_CR2","doi-asserted-by":"publisher","unstructured":"Andrianov, P., Friedberger, K., Mandrykin, M.U., Mutilin, V.S., Volkov, A.: CPA-BAM-BnB: Block-abstraction memoization and region-based memory models for predicate abstractions (competition contribution). In: Proc. TACAS. pp. 355\u2013359. LNCS\u00a010206, Springer (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_22","DOI":"10.1007\/978-3-662-54580-5_22"},{"key":"30_CR3","doi-asserted-by":"publisher","unstructured":"Andrianov, P., Mutilin, V., Khoroshilov, A.: CPALockator: Thread-modular approach with projections (competition contribution). In: Proc. TACAS\u00a0(2). pp. 423\u2013427. LNCS\u00a012652, Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_25","DOI":"10.1007\/978-3-030-72013-1_25"},{"key":"30_CR4","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":"30_CR5","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":"30_CR6","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.: Reproduction package for FM 2024 article \u2018Software verification with CPAchecker 3.0: Tutorial and user guide\u2019. Zenodo (2024). https:\/\/doi.org\/10.5281\/zenodo.13612338","DOI":"10.5281\/zenodo.13612338"},{"key":"30_CR7","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 (extended version). arXiv\/CoRR 2409(02094) (September 2024). https:\/\/doi.org\/10.48550\/arXiv.2409.02094","DOI":"10.48550\/arXiv.2409.02094"},{"key":"30_CR8","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":"30_CR9","unstructured":"Ball, T., Rajamani, S.K.: SLIC: A specification language for interface checking (of\u00a0C). Tech. Rep. MSR-TR-2001-21, Microsoft Research (2002). https:\/\/www.microsoft.com\/en-us\/research\/publication\/slic-a-specification-language-for-interface-checking-of-c\/"},{"key":"30_CR10","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":"30_CR11","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":"30_CR12","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Competition on software verification and witness validation: SV-COMP 2023. In: Proc. TACAS\u00a0(2). pp. 495\u2013522. LNCS\u00a013994, Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_29","DOI":"10.1007\/978-3-031-30820-8_29"},{"key":"30_CR13","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":"30_CR14","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":"30_CR15","doi-asserted-by":"publisher","unstructured":"Beyer, D., Chien, P.C., Lee, N.Z.: CPA-DF: A tool for configurable interval analysis to boost program verification. In: Proc. ASE. pp. 2050\u20132053. IEEE (2023). https:\/\/doi.org\/10.1109\/ASE56229.2023.00213","DOI":"10.1109\/ASE56229.2023.00213"},{"key":"30_CR16","doi-asserted-by":"crossref","unstructured":"Beyer, D., Chien, P.C., Lee, N.Z.: Augmenting interpolation-based model checking with auxiliary invariants. In: Proc. SPIN. Springer (2024)","DOI":"10.1007\/978-3-031-66149-5_13"},{"key":"30_CR17","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":"30_CR18","doi-asserted-by":"publisher","unstructured":"Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software model checking via large-block encoding. In: Proc. FMCAD. pp. 25\u201332. IEEE (2009). https:\/\/doi.org\/10.1109\/FMCAD.2009.5351147","DOI":"10.1109\/FMCAD.2009.5351147"},{"key":"30_CR19","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":"30_CR20","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":"30_CR21","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Wendler, P.: Combining k-induction with continuously-refined invariants. Tech. Rep. MIP-1503, University of Passau (January 2015). https:\/\/doi.org\/10.48550\/arXiv.1502.00096","DOI":"10.48550\/arXiv.1502.00096"},{"key":"30_CR22","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":"30_CR23","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":"30_CR24","doi-asserted-by":"publisher","unstructured":"Beyer, D., Friedberger, K.: In-place vs. copy-on-write CEGAR refinement for block summarization with caching. In: Proc. ISoLA. pp. 197\u2013215. LNCS\u00a011245, Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-03421-4_14","DOI":"10.1007\/978-3-030-03421-4_14"},{"key":"30_CR25","doi-asserted-by":"publisher","unstructured":"Beyer, D., Friedberger, K.: Domain-independent interprocedural program analysis using block-abstraction memoization. In: Proc. ESEC\/FSE. pp. 50\u201362. ACM (2020). https:\/\/doi.org\/10.1145\/3368089.3409718","DOI":"10.1145\/3368089.3409718"},{"key":"30_CR26","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":"30_CR27","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":"30_CR28","doi-asserted-by":"publisher","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Configurable software verification: Concretizing the convergence of model checking and program analysis. In: Proc. CAV. pp. 504\u2013518. LNCS\u00a04590, Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_51","DOI":"10.1007\/978-3-540-73368-3_51"},{"key":"30_CR29","doi-asserted-by":"publisher","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Program analysis with dynamic precision adjustment. In: Proc. ASE. pp. 29\u201338. IEEE (2008). https:\/\/doi.org\/10.1109\/ASE.2008.13","DOI":"10.1109\/ASE.2008.13"},{"key":"30_CR30","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":"30_CR31","doi-asserted-by":"publisher","unstructured":"Beyer, D., Jakobs, M.C.: Fred: Conditional model checking via reducers and folders. In: Proc. SEFM. pp. 113\u2013132. LNCS\u00a012310, Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-58768-0_7","DOI":"10.1007\/978-3-030-58768-0_7"},{"key":"30_CR32","doi-asserted-by":"publisher","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","DOI":"10.1007\/s10009-020-00587-8"},{"key":"30_CR33","doi-asserted-by":"publisher","unstructured":"Beyer, D., Jakobs, M.C., Lemberger, T.: Difference verification with conditions. In: Proc. SEFM. pp. 133\u2013154. LNCS\u00a012310, Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-58768-0_8","DOI":"10.1007\/978-3-030-58768-0_8"},{"key":"30_CR34","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":"30_CR35","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":"30_CR36","unstructured":"Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: Proc. FMCAD. pp. 189\u2013197. FMCAD (2010). https:\/\/dl.acm.org\/doi\/10.5555\/1998496.1998532"},{"key":"30_CR37","doi-asserted-by":"publisher","unstructured":"Beyer, D., Kettl, M., Lemberger, T.: Decomposing software verification using distributed summary synthesis. Proc. ACM Softw. Eng. 1(FSE) (2024). https:\/\/doi.org\/10.1145\/3660766","DOI":"10.1145\/3660766"},{"key":"30_CR38","doi-asserted-by":"publisher","unstructured":"Beyer, D., Lee, N.Z., Wendler, P.: Interpolation and SAT-based model checking revisited: Adoption to software verification. J. Autom. Reasoning (2024). https:\/\/doi.org\/10.1007\/s10817-024-09702-9, preprint: https:\/\/doi.org\/10.48550\/arXiv.2208.05046","DOI":"10.1007\/s10817-024-09702-9 10.48550\/arXiv.2208.05046"},{"key":"30_CR39","doi-asserted-by":"publisher","unstructured":"Beyer, D., Lemberger, T.: Symbolic execution with CEGAR. In: Proc. ISoLA. pp. 195\u2013211. LNCS\u00a09952, Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-47166-2_14","DOI":"10.1007\/978-3-319-47166-2_14"},{"key":"30_CR40","doi-asserted-by":"publisher","unstructured":"Beyer, D., Lemberger, T.: CPA-SymExec: Efficient symbolic execution in CPAchecker. In: Proc. ASE. pp. 900\u2013903. ACM (2018). https:\/\/doi.org\/10.1145\/3238147.3240478","DOI":"10.1145\/3238147.3240478"},{"key":"30_CR41","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":"30_CR42","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":"30_CR43","doi-asserted-by":"publisher","unstructured":"Beyer, D., L\u00f6we, S.: Explicit-state software model checking based on CEGAR and interpolation. In: Proc. FASE. pp. 146\u2013162. LNCS\u00a07793, Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-37057-1_11","DOI":"10.1007\/978-3-642-37057-1_11"},{"key":"30_CR44","doi-asserted-by":"publisher","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Refinement selection. In: Proc. SPIN. pp. 20\u201338. LNCS\u00a09232, Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-23404-5_3","DOI":"10.1007\/978-3-319-23404-5_3"},{"key":"30_CR45","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":"30_CR46","doi-asserted-by":"publisher","unstructured":"Beyer, D., Stahlbauer, A.: BDD-based software model checking with CPAchecker. In: Proc. MEMICS. pp. 1\u201311. LNCS\u00a07721, Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-36046-6_1","DOI":"10.1007\/978-3-642-36046-6_1"},{"key":"30_CR47","doi-asserted-by":"publisher","unstructured":"Beyer, D., Stahlbauer, A.: BDD-based software verification: Applications to event-condition-action systems. Int. J. Softw. Tools Technol. Transfer 16(5), 507\u2013518 (2014). https:\/\/doi.org\/10.1007\/s10009-014-0334-1","DOI":"10.1007\/s10009-014-0334-1"},{"key":"30_CR48","unstructured":"Beyer, D., Wendler, P.: CPAchecker with sequential combination and strategy selection. In: Automatic Software Verification. Springer (2024)"},{"key":"30_CR49","doi-asserted-by":"publisher","unstructured":"Beyer, D., Wendler, P.: CPAchecker releases. Zenodo. https:\/\/doi.org\/10.5281\/zenodo.3816620","DOI":"10.5281\/zenodo.3816620"},{"key":"30_CR50","doi-asserted-by":"publisher","unstructured":"Beyer, D., Wendler, P.: CPAchecker release 3.0. Zenodo (2024). https:\/\/doi.org\/10.5281\/zenodo.12663059","DOI":"10.5281\/zenodo.12663059"},{"key":"30_CR51","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":"30_CR52","doi-asserted-by":"publisher","unstructured":"B\u00fcrdek, J., Lochau, M., Bauregger, S., Holzer, A., von Rhein, A., Apel, S., Beyer, D.: Facilitating reuse in multi-goal test-suite generation for software product lines. In: Proc. FASE. pp. 84\u201399. LNCS\u00a09033, Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46675-9_6","DOI":"10.1007\/978-3-662-46675-9_6"},{"key":"30_CR53","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":"30_CR54","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for the static analysis of programs by construction or approximation of fixpoints. In: Proc. POPL. pp. 238\u2013252. ACM (1977). https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"30_CR55","doi-asserted-by":"publisher","unstructured":"Dangl, M., L\u00f6we, S., Wendler, P.: CPAchecker with support for recursive programs and floating-point arithmetic (competition contribution). In: Proc. TACAS. pp. 423\u2013425. LNCS\u00a09035, Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_34","DOI":"10.1007\/978-3-662-46681-0_34"},{"key":"30_CR56","doi-asserted-by":"publisher","unstructured":"Dudka, K., Peringer, P., Vojnar, T.: Byte-precise verification of low-level list manipulation. In: Proc. SAS. pp. 215\u2013237. LNCS\u00a07935, Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-38856-9_13","DOI":"10.1007\/978-3-642-38856-9_13"},{"key":"30_CR57","doi-asserted-by":"publisher","unstructured":"Friedberger, K.: CPA-BAM: Block-abstraction memoization with value analysis and predicate analysis (competition contribution). In: Proc. TACAS. pp. 912\u2013915. LNCS\u00a09636, Springer (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_58","DOI":"10.1007\/978-3-662-49674-9_58"},{"key":"30_CR58","doi-asserted-by":"publisher","unstructured":"Heizmann, M., Hoenicke, J., Leike, J., Podelski, A.: Linear ranking for linear lasso programs. In: Proc. ATVA. pp. 365\u2013380. LNCS\u00a08172, Springer (2013). https:\/\/doi.org\/10.1007\/978-3-319-02444-8_26","DOI":"10.1007\/978-3-319-02444-8_26"},{"key":"30_CR59","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":"30_CR60","doi-asserted-by":"publisher","unstructured":"Jakobs, M.C.: CoVeriTest with dynamic partitioning of the iteration time limit (competition contribution). In: Proc. FASE. pp. 540\u2013544. LNCS\u00a012076, Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-45234-6_30","DOI":"10.1007\/978-3-030-45234-6_30"},{"key":"30_CR61","doi-asserted-by":"publisher","unstructured":"Jakobs, M.C.: CoVeriTest: Interleaving value and predicate analysis for test-case generation (competition contribution). Int. J. Softw. Tools Technol. Transf. 23(6), 847\u2013851 (December 2021). https:\/\/doi.org\/10.1007\/s10009-020-00572-1","DOI":"10.1007\/s10009-020-00572-1"},{"key":"30_CR62","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":"30_CR63","doi-asserted-by":"publisher","unstructured":"Jhala, R., Podelski, A., Rybalchenko, A.: Predicate abstraction for program verification. In: Handbook of Model Checking, pp. 447\u2013491. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_15","DOI":"10.1007\/978-3-319-10575-8_15"},{"key":"30_CR64","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":"30_CR65","doi-asserted-by":"publisher","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976). https:\/\/doi.org\/10.1145\/360248.360252","DOI":"10.1145\/360248.360252"},{"key":"30_CR66","doi-asserted-by":"publisher","unstructured":"Leeson, W., Dwyer, M.: Graves-CPA: A graph-attention verifier selector (competition contribution). In: Proc. TACAS\u00a0(2). pp. 440\u2013445. LNCS\u00a013244, Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_28","DOI":"10.1007\/978-3-030-99527-0_28"},{"key":"30_CR67","doi-asserted-by":"publisher","unstructured":"Leike, J., Heizmann, M.: Ranking templates for linear loops. Logical Methods in Computer Science 11(1) (2015). https:\/\/doi.org\/10.2168\/LMCS-11(1:16)2015","DOI":"10.2168\/LMCS-11(1:16)2015"},{"key":"30_CR68","doi-asserted-by":"publisher","unstructured":"L\u00f6we, S.: CPAchecker with explicit-value analysis based on CEGAR and interpolation (competition contribution). In: Proc. TACAS. pp. 610\u2013612. LNCS\u00a07795, Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_44","DOI":"10.1007\/978-3-642-36742-7_44"},{"key":"30_CR69","doi-asserted-by":"publisher","unstructured":"L\u00f6we, S., Mandrykin, M.U., Wendler, P.: CPAchecker with sequential combination of explicit-value analyses and predicate analyses (competition contribution). In: Proc. TACAS. pp. 392\u2013394. LNCS\u00a08413, Springer (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_27","DOI":"10.1007\/978-3-642-54862-8_27"},{"key":"30_CR70","doi-asserted-by":"publisher","unstructured":"L\u00f6we, S., Wendler, P.: CPAchecker with adjustable predicate analysis (competition contribution). In: Proc. TACAS. pp. 528\u2013530. LNCS\u00a07214, Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_40","DOI":"10.1007\/978-3-642-28756-5_40"},{"key":"30_CR71","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":"30_CR72","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":"30_CR73","doi-asserted-by":"publisher","unstructured":"Peled, D.: Ten years of partial order reduction. In: Proc. CAV. pp. 17\u201328. Springer (1998). https:\/\/doi.org\/10.1007\/BFb0028727","DOI":"10.1007\/BFb0028727"},{"key":"30_CR74","doi-asserted-by":"publisher","unstructured":"Richter, C., Wehrheim, H.: PeSCo: Predicting sequential combinations of verifiers (competition contribution). In: Proc. TACAS\u00a0(3). pp. 229\u2013233. LNCS\u00a011429, Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_19","DOI":"10.1007\/978-3-030-17502-3_19"},{"key":"30_CR75","doi-asserted-by":"publisher","unstructured":"Ruland, S., Lochau, M., Jakobs, M.C.: HybridTiger: Hybrid model checking and domination-based partitioning for efficient multi-goal test-suite generation (competition contribution). In: Proc. FASE. pp. 520\u2013524. LNCS\u00a012076, Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-45234-6_26","DOI":"10.1007\/978-3-030-45234-6_26"},{"key":"30_CR76","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":"30_CR77","doi-asserted-by":"publisher","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking safety properties using induction and a SAT-solver. In: Proc. FMCAD, pp. 127\u2013144. LNCS\u00a01954, Springer (2000). https:\/\/doi.org\/10.1007\/3-540-40922-X_8","DOI":"10.1007\/3-540-40922-X_8"},{"key":"30_CR78","unstructured":"The Open Group: 64-bit and data size neutrality. https:\/\/unix.org\/whitepapers\/64bit.html, accessed: 2024-06-29"},{"key":"30_CR79","doi-asserted-by":"publisher","unstructured":"Vizel, Y., Grumberg, O.: Interpolation-sequence based model checking. In: Proc. FMCAD. pp.\u00a01\u20138. IEEE (2009). https:\/\/doi.org\/10.1109\/FMCAD.2009.5351148","DOI":"10.1109\/FMCAD.2009.5351148"},{"key":"30_CR80","doi-asserted-by":"publisher","unstructured":"Vizel, Y., Grumberg, O., Shoham, S.: Intertwined forward-backward reachability analysis using interpolants. In: Proc. TACAS. pp. 308\u2013323. LNCS\u00a07795, Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_22","DOI":"10.1007\/978-3-642-36742-7_22"},{"key":"30_CR81","doi-asserted-by":"publisher","unstructured":"Wendler, P.: CPAchecker with sequential combination of explicit-state analysis and predicate analysis (competition contribution). In: Proc. TACAS. pp. 613\u2013615. LNCS\u00a07795, Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_45","DOI":"10.1007\/978-3-642-36742-7_45"},{"key":"30_CR82","doi-asserted-by":"publisher","unstructured":"Wonisch, D.: Block abstraction memoization for CPAchecker (competition contribution). In: Proc. TACAS. pp. 531\u2013533. LNCS\u00a07214, Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_41","DOI":"10.1007\/978-3-642-28756-5_41"},{"key":"30_CR83","doi-asserted-by":"publisher","unstructured":"Wonisch, D., Wehrheim, H.: Predicate analysis with block-abstraction memoization. In: Proc. ICFEM. pp. 332\u2013347. LNCS\u00a07635, Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-34281-3_24","DOI":"10.1007\/978-3-642-34281-3_24"},{"key":"30_CR84","doi-asserted-by":"publisher","unstructured":"Zakharov, I.S., Mandrykin, M.U., Mutilin, V.S., Novikov, E., Petrenko, A.K., Khoroshilov, A.V.: Configurable toolset for static verification of operating systems kernel modules. Programming and Comp. Softw. 41(1), 49\u201364 (2015). https:\/\/doi.org\/10.1134\/S0361768815010065","DOI":"10.1134\/S0361768815010065"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71177-0_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,28]],"date-time":"2024-11-28T01:10:33Z","timestamp":1732756233000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71177-0_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,13]]},"ISBN":["9783031711763","9783031711770"],"references-count":84,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71177-0_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,9,13]]},"assertion":[{"value":"13 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"<scp>CPAchecker<\/scp> was funded in part by the Canadian Natural Sciences and Engineering Research Council (NSERC) \u2014, by the Deutsche Forschungsgemeinschaft (DFG) \u2014(),(),(),(ReVeriX), by the Free State of Bavaria, and by the LMU PostDoc Support Funds.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Funding Statement"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}