Cooperative software verification via dynamic program splitting
Richter C, Chalupa M, Jakobs M-C, Wehrheim H. 2025. Cooperative software verification via dynamic program splitting. 47th International Conference on Software Engineering. ICSE: International Conference on Software Engineering, 2087–2099.
Download
No fulltext has been uploaded. References only!
Conference Paper
| Published
| English
Scopus indexed
Author
Richter, Cedric;
Chalupa, MarekISTA;
Jakobs, Marie-Christine;
Wehrheim, Heike
Corresponding author has ISTA affiliation
Department
Abstract
Cooperative software verification divides the task of software verification among several verification tools in order to increase efficiency and effectiveness. The basic approach is to let verifiers work on different parts of a program and at the end join verification results. While this idea is intuitively appealing, cooperative verification is usually hindered by the fact that program decomposition (1) is often static, disregarding strengths and weaknesses of employed verifiers, and (2) often represents the decomposed program parts in a specific proprietary format, thereby making the use of off-the-shelf verifiers in cooperative verification difficult. In this paper, we propose a novel cooperative verification scheme that we call dynamic program splitting (DPS). Splitting decomposes programs into (smaller) programs, and thus directly enables the use of off-the-shelf tools. In DPS, splitting is dynamically applied on demand: Verification starts by giving a verification task (a program plus a correctness specification) to a verifier V1. Whenever V1 finds the current task to be hard to verify, it splits the task (i.e., the program) and restarts verification on subtasks. DPS continues until (1) a violation is found, (2) all subtasks are completed or (3) some user-defined stopping criterion is met. In the latter case, the remaining uncompleted subtasks are merged into a single one and are given to a next verifier V2, repeating the same procedure on the still unverified program parts. This way, the decomposition is steered by what is hard to verify for particular verifiers, leveraging their complementary strengths. We have implemented dynamic program splitting and evaluated it on benchmarks of the annual software verification competition SV-COMP. The evaluation shows that cooperative verification with DPS is able to solve verification tasks that none of the constituent verifiers can solve, without any significant overhead.
Publishing Year
Date Published
2025-05-01
Proceedings Title
47th International Conference on Software Engineering
Publisher
IEEE
Acknowledgement
This work is partially supported by the German Research Foundation (DFG) – WE2290/13-2 (Coop2), and in part by the ERC-2020-AdG 101020093.
Page
2087-2099
Conference
ICSE: International Conference on Software Engineering
Conference Location
Ottawa, ON, Canada
Conference Date
2025-04-26 – 2025-05-06
ISBN
eISSN
IST-REx-ID
Cite this
Richter C, Chalupa M, Jakobs M-C, Wehrheim H. Cooperative software verification via dynamic program splitting. In: 47th International Conference on Software Engineering. IEEE; 2025:2087-2099. doi:10.1109/ICSE55347.2025.00092
Richter, C., Chalupa, M., Jakobs, M.-C., & Wehrheim, H. (2025). Cooperative software verification via dynamic program splitting. In 47th International Conference on Software Engineering (pp. 2087–2099). Ottawa, ON, Canada: IEEE. https://doi.org/10.1109/ICSE55347.2025.00092
Richter, Cedric, Marek Chalupa, Marie-Christine Jakobs, and Heike Wehrheim. “Cooperative Software Verification via Dynamic Program Splitting.” In 47th International Conference on Software Engineering, 2087–99. IEEE, 2025. https://doi.org/10.1109/ICSE55347.2025.00092.
C. Richter, M. Chalupa, M.-C. Jakobs, and H. Wehrheim, “Cooperative software verification via dynamic program splitting,” in 47th International Conference on Software Engineering, Ottawa, ON, Canada, 2025, pp. 2087–2099.
Richter C, Chalupa M, Jakobs M-C, Wehrheim H. 2025. Cooperative software verification via dynamic program splitting. 47th International Conference on Software Engineering. ICSE: International Conference on Software Engineering, 2087–2099.
Richter, Cedric, et al. “Cooperative Software Verification via Dynamic Program Splitting.” 47th International Conference on Software Engineering, IEEE, 2025, pp. 2087–99, doi:10.1109/ICSE55347.2025.00092.