{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:25:03Z","timestamp":1779074703910,"version":"3.51.4"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032009418","type":"print"},{"value":"9783032009425","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,8,28]],"date-time":"2025-08-28T00:00:00Z","timestamp":1756339200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,8,28]],"date-time":"2025-08-28T00:00:00Z","timestamp":1756339200000},"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>Software model checking and deductive software verification have complementary strengths and weaknesses: software model checkers are more straight-forward to use, as they analyze\u00a0the program without user input; but they do not yet support complicated data structures and expressive specifications. In contrast, deductive verifiers can verify expressive specifications and complex data structures modularly, but they require the user to specify\u00a0the program behavior in detail, which is a time-consuming process.\u00a0Due to their differing nature, the two approaches usually remain separate. However, for industrial usage, one requires both: ease\u00a0of use as well as expressiveness. Therefore, we present <jats:sc>AutoSV-Annotator<\/jats:sc>,\u00a0a toolchain that integrates the two approaches for C\u00a0programs.\u00a0The toolchain allows a user to iteratively refine the deductive annotations in a C\u00a0program, calling a model checker to supplement the annotations at each iteration, guided by the already existing annotations. We show that our tool is able to annotate and\u00a0prove many tasks from the SV-Benchmarks set. Our results show that the\u00a0two strategies can indeed benefit from each other.<\/jats:p>","DOI":"10.1007\/978-3-032-00942-5_4","type":"book-chapter","created":{"date-parts":[[2025,8,27]],"date-time":"2025-08-27T12:03:44Z","timestamp":1756296224000},"page":"59-77","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["AutoSV-Annotator: Integrating Deductive and Automatic Software Verification"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7565-0954","authenticated-orcid":false,"given":"Lukas","family":"Armborst","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-0003-4467-072X","authenticated-orcid":false,"given":"Marieke","family":"Huisman","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"}]}],"member":"297","published-online":{"date-parts":[[2025,8,28]]},"reference":[{"key":"4_CR1","doi-asserted-by":"publisher","unstructured":"Alshnakat, A., Gurov, D., Lidstr\u00f6m, C., R\u00fcmmer, P.: Constraint-Based Contract Inference for Deductive Verification, pp. 149\u2013176. LNCS\u00a012345, Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-64354-6_6","DOI":"10.1007\/978-3-030-64354-6_6"},{"key":"4_CR2","doi-asserted-by":"publisher","unstructured":"Amighi, A., Haack, C., Huisman, M., Hurlin, C.: Permission-based separation logic for multithreaded Java programs. LMCS 11(1) (2015). https:\/\/doi.org\/10.2168\/LMCS-11(1:2)2015","DOI":"10.2168\/LMCS-11(1:2)2015"},{"key":"4_CR3","doi-asserted-by":"publisher","unstructured":"Amilon, J., Esen, Z., Gurov, D., Lidstr\u00f6m, C., R\u00fcmmer, P.: An Exercise in Mind Reading: Automatic Contract Inference for Frama-C. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-55608-1_13","DOI":"10.1007\/978-3-031-55608-1_13"},{"key":"4_CR4","doi-asserted-by":"publisher","unstructured":"Armborst, L., Beyer, D., Huisman, M., Lingsch-Rosenfeld, M.: Reproduction package for FMICS2025 Submission \u2018AutoSV-Annotator: Integrating Deductive and Automatic Software Verification\u2019. Zenodo (2025). https:\/\/doi.org\/10.5281\/zenodo.15199589","DOI":"10.5281\/zenodo.15199589"},{"key":"4_CR5","doi-asserted-by":"publisher","unstructured":"Armborst, L., Bos, P., van\u00a0den Haak, L., Huisman, M., Rubbens, R., \u015eakar, O., Tasche, P.: The VerCors verifier: A progress report. In: Proc. CAV. pp. 3\u201318. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-65630-9_1","DOI":"10.1007\/978-3-031-65630-9_1"},{"key":"4_CR6","unstructured":"Armborst, L., Huisman, M.: Using Horn solvers to generate memory access permissions for deductive verification: A preliminary report (2024)"},{"key":"4_CR7","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":"4_CR8","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":"4_CR9","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":"4_CR10","doi-asserted-by":"publisher","unstructured":"Beckert, B., Kirsten, M., Klamroth, J., Ulbrich, M.: Modular verification of JML contracts using bounded model checking. In: Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-61362-4_4","DOI":"10.1007\/978-3-030-61362-4_4"},{"key":"4_CR11","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":"4_CR12","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M.: Software verification with PDR: An implementation of the state of the art. In: Proc. TACAS\u00a0(1). pp. 3\u201321. LNCS\u00a012078, Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_1","DOI":"10.1007\/978-3-030-45190-5_1"},{"key":"4_CR13","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":"4_CR14","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":"4_CR15","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":"4_CR16","doi-asserted-by":"publisher","unstructured":"Beyer, D., Lingsch-Rosenfeld, M.: CPAchecker 4.0 as Witness Validator (Competition Contribution). In: Proc. TACAS\u00a0(3). pp. 192\u2013198. LNCS\u00a015698, Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-90660-2_11","DOI":"10.1007\/978-3-031-90660-2_11"},{"key":"4_CR17","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":"4_CR18","doi-asserted-by":"publisher","unstructured":"Beyer, D., Spiessl, M., Umbricht, S.: Cooperation between automatic and interactive software verifiers. In: Proc. SEFM. p. 111\u2013128. 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":"4_CR19","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":"4_CR20","doi-asserted-by":"publisher","unstructured":"Beyer, D., Wachowitz, H.: FM-Weck: Containerized execution of formal-methods tools. In: Proc. FM. pp. 39\u201347. LNCS\u00a014934, Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-71177-0_3","DOI":"10.1007\/978-3-031-71177-0_3"},{"key":"4_CR21","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":"4_CR22","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":"4_CR23","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":"4_CR24","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":"4_CR25","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT (1999)"},{"key":"4_CR26","doi-asserted-by":"publisher","unstructured":"Cok, D.: OpenJML: software verification for Java 7 using JML, OpenJDK, and Eclipse. In: 1st Workshop on Formal Integrated Development Environment, (F-IDE). pp. 79\u201392 (2014). https:\/\/doi.org\/10.4204\/EPTCS.149.8","DOI":"10.4204\/EPTCS.149.8"},{"key":"4_CR27","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":"4_CR28","doi-asserted-by":"publisher","unstructured":"Dohrau, J.: Automatic Inference of Permission Specifications. Ph.D. thesis, ETH Zurich (2022). https:\/\/doi.org\/10.3929\/ethz-b-000588977","DOI":"10.3929\/ethz-b-000588977"},{"key":"4_CR29","doi-asserted-by":"publisher","unstructured":"Donaldson, A.F., Haller, L., Kr\u00f6ning, D., R\u00fcmmer, P.: Software verification using k-induction. In: Proc. SAS. pp. 351\u2013368. LNCS\u00a06887, Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-23702-7_26","DOI":"10.1007\/978-3-642-23702-7_26"},{"key":"4_CR30","doi-asserted-by":"publisher","unstructured":"Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The Daikon system for dynamic detection of likely invariants. Science of Computer Programming 69(1\u20133), 35\u201345 (2007). https:\/\/doi.org\/10.1016\/j.scico.2007.01.015, Tool website: https:\/\/plse.cs.washington.edu\/daikon\/","DOI":"10.1016\/j.scico.2007.01.015"},{"key":"4_CR31","doi-asserted-by":"publisher","unstructured":"Ezudheen, P., Neider, D., D\u2019Souza, D., Garg, P., Madhusudan, P.: Horn-ICE learning for synthesizing invariants and contracts. Proc. ACM Program. Lang. 2(OOPSLA) (2018). https:\/\/doi.org\/10.1145\/3276501","DOI":"10.1145\/3276501"},{"key":"4_CR32","doi-asserted-by":"publisher","unstructured":"Galeotti, J., Furia, C., May, E., Fraser, G., Zeller, A.: Inferring loop invariants by mutation, dynamic analysis, and static checking. IEEE Trans. Softw. Eng. 41, 1019\u20131037 (2015). https:\/\/doi.org\/10.1109\/TSE.2015.2431688","DOI":"10.1109\/TSE.2015.2431688"},{"key":"4_CR33","doi-asserted-by":"publisher","unstructured":"H\u00e4hnle, R., Huisman, M.: Deductive software verification: From pen-and-paper proofs to industrial tools. In: Computing and Software Science - State of the Art and Perspectives, pp. 345\u2013373. LNCS\u00a010000, Springer (2019). https:\/\/doi.org\/10.1007\/978-3-319-91908-9_18","DOI":"10.1007\/978-3-319-91908-9_18"},{"key":"4_CR34","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":"4_CR35","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":"4_CR36","doi-asserted-by":"publisher","unstructured":"Heizmann, M., Klumpp, D., Lingsch-Rosenfeld, M., Sch\u00fcssele, F.: Correctness Witnesses with Function Contracts. arXiv (1 2025). https:\/\/doi.org\/10.48550\/arXiv.2501.12313","DOI":"10.48550\/arXiv.2501.12313"},{"key":"4_CR37","unstructured":"Janssen, D.D.: Design and implementation of new features for runtime permission verification in concurrent Java programs using VerCors (May 2024)"},{"key":"4_CR38","doi-asserted-by":"publisher","unstructured":"Jon\u00e1\u0161, M., Kumor, K., Nov\u00e1k, J., Sedl\u00e1cek, J., Trt\u00edk, M., Zaoral, L., Ayaziov\u00e1, P., Strejcek, 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"},{"issue":"7","key":"4_CR39","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976). https:\/\/doi.org\/10.1145\/360248.360252","journal-title":"Commun. ACM"},{"key":"4_CR40","doi-asserted-by":"publisher","unstructured":"Lathouwers, S., Huisman, M.: Survey of annotation generators for deductive verifiers. Journal of Systems and Software 211 (2024). https:\/\/doi.org\/10.1016\/j.jss.2024.111972","DOI":"10.1016\/j.jss.2024.111972"},{"key":"4_CR41","unstructured":"Leavens, G., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D.R., M\u00fcller, P., Kiniry, J., Chalin, P.: JML Reference Manual (2007), Dept. of Computer Science, Iowa State University. Available from http:\/\/www.jmlspecs.org"},{"key":"4_CR42","doi-asserted-by":"publisher","unstructured":"McMillan, K.L., Padon, O.: Ivy: A multi-modal verification tool for distributed algorithms. In: Lahiri, S.K., Wang, C. (eds.) Proc. CAV. Springer International Publishing (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_12","DOI":"10.1007\/978-3-030-53291-8_12"},{"key":"4_CR43","doi-asserted-by":"publisher","unstructured":"Saan, S., Erhard, J., Schwarz, M., Bozhilov, S., Holter, K., Tilscher, S., Vojdani, V., Seidl, H.: Goblint Validator: Correctness witness validation by abstract interpretation (competition contribution). In: Proc. TACAS\u00a0(3). pp. 335\u2013340. LNCS\u00a014572, Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_17","DOI":"10.1007\/978-3-031-57256-2_17"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-00942-5_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,27]],"date-time":"2025-08-27T12:03:47Z","timestamp":1756296227000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-00942-5_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,28]]},"ISBN":["9783032009418","9783032009425"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-00942-5_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,8,28]]},"assertion":[{"value":"28 August 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"FMICS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Methods for Industrial Critical Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Aarhus","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Denmark","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":"27 August 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 August 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fmics2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/FMICS2025.uni-muenster.de","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}