{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,29]],"date-time":"2026-01-29T20:49:19Z","timestamp":1769719759325,"version":"3.49.0"},"publisher-location":"Cham","reference-count":56,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031787492","type":"print"},{"value":"9783031787508","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,2,12]],"date-time":"2025-02-12T00:00:00Z","timestamp":1739318400000},"content-version":"vor","delay-in-days":42,"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>\n                  <jats:p>\n                    We present\n                    <jats:sc>CPA-Daemon<\/jats:sc>\n                    , a microservice for continuous software verification of C code.\n                    <jats:sc>CPA-Daemon<\/jats:sc>\n                    provides full access to the verifier\n                    <jats:sc>CPAchecker<\/jats:sc>\n                    , but adds a clear network interface based on gRPC that abstracts from three different modes of execution: (1)\u00a0running\n                    <jats:sc>CPAchecker<\/jats:sc>\n                    in a separate JVM, (2)\u00a0running\u00a0\n                    <jats:sc>CPAchecker<\/jats:sc>\n                    as a native executable compiled with GraalVM, and (3)\u00a0running\u00a0\n                    <jats:sc>CPAchecker<\/jats:sc>\n                    in a shared, continuously-running JVM. The last two are novel execution modes that greatly improve the response time of verification in different verification scenarios and enable the seamless integration of\n                    <jats:sc>CPAchecker<\/jats:sc>\n                    as an engine in other verification tooling. Our comparative evaluation shows that\n                    <jats:sc>CPA-Daemon<\/jats:sc>\n                    reduces the response time on small verification tasks down to 17%, and that it can reduce the response\u00a0time of existing cooperative verification techniques down to 70%. While our implementation focuses on\n                    <jats:sc>CPAchecker<\/jats:sc>\n                    , the conceptual ideas are of general nature and can serve as a solution for other verification tools that face similar JVM-specific issues.\n                    <jats:sc>CPA-Daemon<\/jats:sc>\n                    is open source and available at\n                    <jats:ext-link xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" xlink:href=\"https:\/\/gitlab.com\/sosy-lab\/software\/cpa-daemon\" ext-link-type=\"uri\">https:\/\/gitlab.com\/sosy-lab\/software\/cpa-daemon<\/jats:ext-link>\n                    .\n                  <\/jats:p>","DOI":"10.1007\/978-3-031-78750-8_8","type":"book-chapter","created":{"date-parts":[[2025,2,11]],"date-time":"2025-02-11T12:15:51Z","timestamp":1739276151000},"page":"158-173","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["CPA-Daemon: Mitigating Tool Restarts for Java-Based Verifiers"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4832-7662","authenticated-orcid":false,"given":"Dirk","family":"Beyer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0291-815X","authenticated-orcid":false,"given":"Thomas","family":"Lemberger","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"}]}],"member":"297","published-online":{"date-parts":[[2025,2,12]]},"reference":[{"key":"8_CR1","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":"8_CR2","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"},{"key":"8_CR3","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":"8_CR4","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":"8_CR5","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":"8_CR6","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":"8_CR7","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":"8_CR8","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":"8_CR9","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"},{"key":"8_CR10","doi-asserted-by":"publisher","unstructured":"Richter, C., H\u00fcllermeier, E., Jakobs, M.C., Wehrheim, H.: Algorithm selection for software validation based on graph kernels. Autom. Softw. Eng. 27(1), 153\u2013186 (2020). https:\/\/doi.org\/10.1007\/s10515-020-00270-x","DOI":"10.1007\/s10515-020-00270-x"},{"key":"8_CR11","doi-asserted-by":"publisher","unstructured":"Novikov, E., Zakharov, I.S.: Towards automated static verification of GNU C programs. In: Proc. PSI. pp. 402\u2013416. LNCS\u00a010742, Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-74313-4_30","DOI":"10.1007\/978-3-319-74313-4_30"},{"key":"8_CR12","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":"8_CR13","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"},{"key":"8_CR14","doi-asserted-by":"publisher","unstructured":"Yin, B., Chen, L., Liu, J., and P.\u00a0Cousot, J.: Verifying numerical programs via iterative abstract testing. In: Proc. SAS. pp. 247\u2013267. LNCS\u00a011822, Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-32304-2_13","DOI":"10.1007\/978-3-030-32304-2_13"},{"key":"8_CR15","doi-asserted-by":"publisher","unstructured":"Pauck, F., Wehrheim, H.: Together strong: Cooperative Android App analysis. In: Proc. ESEC\/FSE. pp. 374\u2013384. ACM (2019). https:\/\/doi.org\/10.1145\/3338906.3338915","DOI":"10.1145\/3338906.3338915"},{"key":"8_CR16","doi-asserted-by":"publisher","unstructured":"Yang, G., Do, Q.C.D., Wen, J.: Distributed assertion checking using symbolic execution. ACM SIGSOFT Softw. Eng. Notes 40(6), \u00a01\u20135 (2015). https:\/\/doi.org\/10.1145\/2830719.2830729","DOI":"10.1145\/2830719.2830729"},{"key":"8_CR17","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":"8_CR18","doi-asserted-by":"publisher","unstructured":"Inverso, O., Trubiani, C.: Parallel and distributed bounded model checking of multi-threaded programs. In: Proc. PPoPP. pp. 202\u2013216. ACM (2020). https:\/\/doi.org\/10.1145\/3332466.3374529","DOI":"10.1145\/3332466.3374529"},{"key":"8_CR19","doi-asserted-by":"publisher","unstructured":"Nguyen, T.L., Schrammel, P., Fischer, B., La\u00a0Torre, S., Parlato, G.: Parallel bug-finding in concurrent programs via reduced interleaving instances. In: Proc. ASE. pp. 753\u2013764. IEEE (2017). https:\/\/doi.org\/10.1109\/ASE.2017.8115686","DOI":"10.1109\/ASE.2017.8115686"},{"key":"8_CR20","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":"8_CR21","unstructured":"Google: gRPC. https:\/\/grpc.io\/, accessed: 2024-08-26"},{"key":"8_CR22","unstructured":"Oracle: GraalVM. https:\/\/www.graalvm.org\/, accessed: 2024-08-26"},{"key":"8_CR23","unstructured":"Collection of verification tasks. https:\/\/gitlab.com\/sosy-lab\/benchmarking\/sv-benchmarks, accessed: 2024-08-26"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Beyer, D., Lee, N.Z.: The transformation game: Joining forces for verification. In: Proc. Festschrift Katoen 60th Birthday. Springer (2024), https:\/\/www.sosy-lab.org\/research\/pub\/2024-Katoen60.The_Transformation_Game_Joining_Forces_for_Verification.pdf","DOI":"10.1007\/978-3-031-75778-5_9"},{"key":"8_CR25","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":"8_CR26","doi-asserted-by":"publisher","unstructured":"Alt, L., Asadi, S., Chockler, H., Even-Mendoza, K., Fedyukovich, G., Hyv\u00e4rinen, A.E.J., Sharygina, N.: HiFrog: SMT-based function summarization for software verification. In: Proc. TACAS. pp. 207\u2013213. LNCS\u00a010206 (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_12","DOI":"10.1007\/978-3-662-54580-5_12"},{"key":"8_CR27","doi-asserted-by":"publisher","unstructured":"Asadi, S., Blicha, M., Hyv\u00e4rinen, A.E.J., Fedyukovich, G., Sharygina, N.: SMT-based verification of program changes through summary repair. Formal Methods Syst. Des. 60(3), 350\u2013380 (2022). https:\/\/doi.org\/10.1007\/s10703-023-00423-0","DOI":"10.1007\/s10703-023-00423-0"},{"key":"8_CR28","doi-asserted-by":"publisher","unstructured":"Calcagno, C., Distefano, D., Dubreil, J., Gabi, D., Hooimeijer, P., Luca, M., O\u2019Hearn, P.W., Papakonstantinou, I., Purbrick, J., Rodriguez, D.: Moving fast with software verification. In: Proc. NFM. pp. 3\u201311. LNCS\u00a09058, Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-17524-9_1","DOI":"10.1007\/978-3-319-17524-9_1"},{"key":"8_CR29","doi-asserted-by":"publisher","unstructured":"Seidl, H., Erhard, J., Vogler, R.: Incremental abstract interpretation. In: From Lambda Calculus to Cybersecurity Through Program Analysis - Essays Dedicated to Chris Hankin on the Occasion of His Retirement. pp. 132\u2013148. LNCS\u00a012065, Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-41103-9_5","DOI":"10.1007\/978-3-030-41103-9_5"},{"key":"8_CR30","doi-asserted-by":"publisher","unstructured":"Beyer, D., L\u00f6we, S., Novikov, E., Stahlbauer, A., Wendler, P.: Precision reuse for efficient regression verification. In: Proc. FSE. pp. 389\u2013399. ACM (2013). https:\/\/doi.org\/10.1145\/2491411.2491429","DOI":"10.1145\/2491411.2491429"},{"key":"8_CR31","doi-asserted-by":"publisher","unstructured":"Barnat, J., Havl\u00edcek, J., Rockai, P.: Distributed LTL model checking with hash compaction. ENTCS 296, 79\u201393 (2013). https:\/\/doi.org\/10.1016\/j.entcs.2013.07.006","DOI":"10.1016\/j.entcs.2013.07.006"},{"key":"8_CR32","doi-asserted-by":"publisher","unstructured":"Yang, G., Qiu, R., Khurshid, S., Pasareanu, C.S., Wen, J.: A synergistic approach to improving symbolic execution using test ranges. Innov. Syst. Softw. Eng. 15(3-4), 325\u2013342 (2019). https:\/\/doi.org\/10.1007\/s11334-019-00331-9","DOI":"10.1007\/s11334-019-00331-9"},{"key":"8_CR33","doi-asserted-by":"publisher","unstructured":"Brain, M., Schanda, F.: A lightweight technique for distributed and incremental program verification. In: Proc. VSTTE. pp. 114\u2013129. LNCS\u00a07152, Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-27705-4_10","DOI":"10.1007\/978-3-642-27705-4_10"},{"key":"8_CR34","doi-asserted-by":"publisher","unstructured":"Lopes, N.P., Rybalchenko, A.: Distributed and predictable software model checking. In: Proc. VMCAI. pp. 340\u2013355. LNCS\u00a06538, Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_24","DOI":"10.1007\/978-3-642-18275-4_24"},{"key":"8_CR35","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":"8_CR36","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":"8_CR37","unstructured":"Dietsch, D., Klumpp, D., Sch\u00fcssele, F., Heizmann, M.: Ultimate repository. https:\/\/github.com\/ultimate-pa\/ultimate, accessed: 2024-08-26"},{"key":"8_CR38","doi-asserted-by":"publisher","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Proc. CAV. pp. 36\u201352. LNCS\u00a08044, Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_2","DOI":"10.1007\/978-3-642-39799-8_2"},{"key":"8_CR39","doi-asserted-by":"publisher","unstructured":"Heizmann, M., Barth, M., Dietsch, D., Fichtner, L., Hoenicke, J., Klumpp, D., Naouar, M., Schindler, T., Sch\u00fcssele, F., Podelski, A.: Ultimate Automizer 2023 (competition contribution). In: Proc. TACAS\u00a0(2). pp. 577\u2013581. LNCS\u00a013994, Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_39","DOI":"10.1007\/978-3-031-30820-8_39"},{"key":"8_CR40","doi-asserted-by":"publisher","unstructured":"Nutz, A., Dietsch, D., Mohamed, M.M., Podelski, A.: Ultimate Kojak with memory safety checks (competition contribution). In: Proc. TACAS. pp. 458\u2013460. LNCS\u00a09035, Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_44","DOI":"10.1007\/978-3-662-46681-0_44"},{"key":"8_CR41","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":"8_CR42","doi-asserted-by":"publisher","unstructured":"Klumpp, D., Dietsch, D., Heizmann, M., Sch\u00fcssele, F., Ebbinghaus, M., Farzan, A., Podelski, A.: Ultimate GemCutter and the axes of generalization (competition contribution). In: Proc. TACAS\u00a0(2). pp. 479\u2013483. LNCS\u00a013244, Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_35","DOI":"10.1007\/978-3-030-99527-0_35"},{"key":"8_CR43","unstructured":"RedHat: Quarkus. https:\/\/quarkus.io\/, accessed: 2024-08-26"},{"key":"8_CR44","doi-asserted-by":"publisher","unstructured":"Beyer, D., Kanav, S., Wachowitz, H.: CoVeriTeam Service: Verification as a service. In: Proc. ICSE, companion. pp. 21\u201325. IEEE (2023). https:\/\/doi.org\/10.1109\/ICSE-Companion58688.2023.00017","DOI":"10.1109\/ICSE-Companion58688.2023.00017"},{"key":"8_CR45","unstructured":"Beyer, D.: Conservation and accessibility of tools for formal methods. In: Proc. Festschrift Podelski 65th Birthday. Springer (2024), https:\/\/www.sosy-lab.org\/research\/pub\/2024-Podelski65.Conservation_and_Accessibility_of_Tools_for_Formal_Methods.pdf"},{"key":"8_CR46","unstructured":"Beyer, D.: Tools for formal methods. https:\/\/fm-tools.sosy-lab.org\/, accessed: 2024-08-26"},{"key":"8_CR47","doi-asserted-by":"publisher","unstructured":"Va\u0161\u00ed\u010dek, O., Fiedor, J., Kratochv\u00edla, T., Bohuslav, K., Smr\u010dka, A., Vojnar, T.: Unite: An Adapter for Transforming Analysis Tools to Web Services via OSLC. In: Proc. ESEC\/FSE. ACM (2022). https:\/\/doi.org\/10.1145\/3540250.3558939","DOI":"10.1145\/3540250.3558939"},{"key":"8_CR48","unstructured":"Synposis: Black duck open hub: CPAchecker. https:\/\/openhub.net\/p\/cpachecker, accessed: 2024-08-26"},{"key":"8_CR49","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":"8_CR50","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT (1999), https:\/\/www.worldcat.org\/isbn\/978-0-2620-3270-4"},{"key":"8_CR51","doi-asserted-by":"publisher","unstructured":"Beyer, D.: SV-Benchmarks: Benchmark set for software verification and testing (SV-COMP 2023 and Test-Comp 2023). Zenodo (2023). https:\/\/doi.org\/10.5281\/zenodo.7627783","DOI":"10.5281\/zenodo.7627783"},{"key":"8_CR52","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":"8_CR53","doi-asserted-by":"publisher","unstructured":"Beyer, D., Lemberger, T., Wachowitz, H.: CPA-Daemon release 1.0. Zenodo (2024). https:\/\/doi.org\/10.5281\/zenodo.13373907","DOI":"10.5281\/zenodo.13373907"},{"key":"8_CR54","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":"8_CR55","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":"8_CR56","doi-asserted-by":"publisher","unstructured":"Beyer, D., Lemberger, T., Wachowitz, H.: Reproduction package for ATVA\u00a02024 submission \u2018CPA-Daemon: Mitigating tool restarts for Java-based verifiers\u2019. Zenodo (2024). https:\/\/doi.org\/10.5281\/zenodo.11147333","DOI":"10.5281\/zenodo.11147333"}],"updated-by":[{"DOI":"10.1007\/978-3-031-78750-8_14","type":"correction","label":"Correction","source":"publisher","updated":{"date-parts":[[2026,1,20]],"date-time":"2026-01-20T00:00:00Z","timestamp":1768867200000}}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-78750-8_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,29]],"date-time":"2026-01-29T10:08:36Z","timestamp":1769681316000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-78750-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031787492","9783031787508"],"references-count":56,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-78750-8_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"12 February 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"20 January 2026","order":2,"name":"change_date","label":"Change Date","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"Correction","order":3,"name":"change_type","label":"Change Type","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"A correction has been published.","order":4,"name":"change_details","label":"Change Details","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CPA-Daemon\n                      release 1.0 is freely available\u00a0[\n                      \n                      ]. The tools that we used for our experiments and all data are available as reproduction artifact\u00a0[\n                      \n                      ] and at:","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Data-Availability Statement"}},{"value":"ATVA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Automated Technology for Verification and Analysis","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Kyoto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","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":"21 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}