AutoSV-Annotator: Integrating Deductive and Automatic Software Verification. Armborst, L., Beyer, D., Huisman, M., & Lingsch-Rosenfeld, M. In Remke, A. & Steffen, B., editors, Formal Methods for Industrial Critical Systems, pages 59–77, Cham, 2025. Springer Nature Switzerland. abstract bibtex Software model checking and deductive software verification have complementary strengths and weaknesses: software model checkers are more straight-forward to use, as they analyze the 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 the program behavior in detail, which is a time-consuming process. Due to their differing nature, the two approaches usually remain separate. However, for industrial usage, one requires both: ease of use as well as expressiveness. Therefore, we present AutoSV-Annotator, a toolchain that integrates the two approaches for C programs. The toolchain allows a user to iteratively refine the deductive annotations in a C program, 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 prove many tasks from the SV-Benchmarks set. Our results show that the two strategies can indeed benefit from each other.
@InProceedings{10.1007/978-3-032-00942-5_4,
author="Armborst, Lukas
and Beyer, Dirk
and Huisman, Marieke
and Lingsch-Rosenfeld, Marian",
editor="Remke, Anne
and Steffen, Bernhard",
title="AutoSV-Annotator: Integrating Deductive and Automatic Software Verification",
booktitle="Formal Methods for Industrial Critical Systems",
year="2025",
publisher="Springer Nature Switzerland",
address="Cham",
pages="59--77",
abstract="Software model checking and deductive software verification have complementary strengths and weaknesses: software model checkers are more straight-forward to use, as they analyze the 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 the program behavior in detail, which is a time-consuming process. Due to their differing nature, the two approaches usually remain separate. However, for industrial usage, one requires both: ease of use as well as expressiveness. Therefore, we present AutoSV-Annotator, a toolchain that integrates the two approaches for C programs. The toolchain allows a user to iteratively refine the deductive annotations in a C program, 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 prove many tasks from the SV-Benchmarks set. Our results show that the two strategies can indeed benefit from each other.",
isbn="978-3-032-00942-5"
}
Downloads: 0
{"_id":"h3TLP9ZsGyxK7ihTT","bibbaseid":"armborst-beyer-huisman-lingschrosenfeld-autosvannotatorintegratingdeductiveandautomaticsoftwareverification-2025","author_short":["Armborst, L.","Beyer, D.","Huisman, M.","Lingsch-Rosenfeld, M."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"propositions":[],"lastnames":["Armborst"],"firstnames":["Lukas"],"suffixes":[]},{"propositions":[],"lastnames":["Beyer"],"firstnames":["Dirk"],"suffixes":[]},{"propositions":[],"lastnames":["Huisman"],"firstnames":["Marieke"],"suffixes":[]},{"propositions":[],"lastnames":["Lingsch-Rosenfeld"],"firstnames":["Marian"],"suffixes":[]}],"editor":[{"propositions":[],"lastnames":["Remke"],"firstnames":["Anne"],"suffixes":[]},{"propositions":[],"lastnames":["Steffen"],"firstnames":["Bernhard"],"suffixes":[]}],"title":"AutoSV-Annotator: Integrating Deductive and Automatic Software Verification","booktitle":"Formal Methods for Industrial Critical Systems","year":"2025","publisher":"Springer Nature Switzerland","address":"Cham","pages":"59–77","abstract":"Software model checking and deductive software verification have complementary strengths and weaknesses: software model checkers are more straight-forward to use, as they analyze the 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 the program behavior in detail, which is a time-consuming process. Due to their differing nature, the two approaches usually remain separate. However, for industrial usage, one requires both: ease of use as well as expressiveness. Therefore, we present AutoSV-Annotator, a toolchain that integrates the two approaches for C programs. The toolchain allows a user to iteratively refine the deductive annotations in a C program, 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 prove many tasks from the SV-Benchmarks set. Our results show that the two strategies can indeed benefit from each other.","isbn":"978-3-032-00942-5","bibtex":"@InProceedings{10.1007/978-3-032-00942-5_4,\nauthor=\"Armborst, Lukas\nand Beyer, Dirk\nand Huisman, Marieke\nand Lingsch-Rosenfeld, Marian\",\neditor=\"Remke, Anne\nand Steffen, Bernhard\",\ntitle=\"AutoSV-Annotator: Integrating Deductive and Automatic Software Verification\",\nbooktitle=\"Formal Methods for Industrial Critical Systems\",\nyear=\"2025\",\npublisher=\"Springer Nature Switzerland\",\naddress=\"Cham\",\npages=\"59--77\",\nabstract=\"Software model checking and deductive software verification have complementary strengths and weaknesses: software model checkers are more straight-forward to use, as they analyze the 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 the program behavior in detail, which is a time-consuming process. Due to their differing nature, the two approaches usually remain separate. However, for industrial usage, one requires both: ease of use as well as expressiveness. Therefore, we present AutoSV-Annotator, a toolchain that integrates the two approaches for C programs. The toolchain allows a user to iteratively refine the deductive annotations in a C program, 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 prove many tasks from the SV-Benchmarks set. Our results show that the two strategies can indeed benefit from each other.\",\nisbn=\"978-3-032-00942-5\"\n}\n\n","author_short":["Armborst, L.","Beyer, D.","Huisman, M.","Lingsch-Rosenfeld, M."],"editor_short":["Remke, A.","Steffen, B."],"key":"10.1007/978-3-032-00942-5_4","id":"10.1007/978-3-032-00942-5_4","bibbaseid":"armborst-beyer-huisman-lingschrosenfeld-autosvannotatorintegratingdeductiveandautomaticsoftwareverification-2025","role":"author","urls":{},"metadata":{"authorlinks":{}},"html":""},"bibtype":"inproceedings","biburl":"https://raw.githubusercontent.com/utwente-fmt/vercors-web/master/static/references.bib","dataSources":["cCvCnPTRQYq3qPe9y"],"keywords":[],"search_terms":["autosv","annotator","integrating","deductive","automatic","software","verification","armborst","beyer","huisman","lingsch-rosenfeld"],"title":"AutoSV-Annotator: Integrating Deductive and Automatic Software Verification","year":2025}