Off-the-Shelf cooperative software verification by splitting programs dynamically

conference paper Off-the-Shelf cooperative software verification by splitting programs dynamically Lecture Notes in Informatics published yes Cedric Richter author Marek Chalupa author 87e34708-d6c6-11ec-9f5b-9391e7be2463 Marie Christine Jakobs author Heike Wehrheim author ToHe department SE: Software Engineering Cooperative software verification aims at improving the effectiveness and efficiency of software verification by enabling multiple verification tools to work together. Existing cooperative verification schemes, however, typically require specialized interfaces or tight integration, limiting their practical applicability. In our International Conference on Software Engineering (ICSE) 2025 publication, we introduce dynamic program splitting – a novel approach that enables cooperation between off-the-shelf verification tools without requiring any modifications. The key idea is to probe verification tools on a given verification task under a time limit and split tasks dynamically that cannot be verified under the given time constraints. The process continues recursively, incrementally identifying program parts that are particularly hard for the given verifier. The remaining unverified parts are provided to a second verifier, allowing to leverage the complementary strengths of different tools. Our evaluation on SV-COMP benchmarks demonstrates that cooperation through dynamic program splitting enables the verification of tasks that none of the individual verifiers can solve on their own. https://research-explorer.ista.ac.at/download/22622/23170/2026_LNI_Richter.pdf application/pdfno https://creativecommons.org/licenses/by-sa/4.0/ Gesellschaft für Informatik2026Bonn, Switzerland eng Software VerificationCooperationProgram Decomposition Software Engineering 2026 1617-546810.18420/se2026_45 P-37741-42 C. Richter, M. Chalupa, M. C. Jakobs, and H. Wehrheim, “Off-the-Shelf cooperative software verification by splitting programs dynamically,” in Software Engineering 2026, Bonn, Switzerland, 2026, vol. P-377, pp. 41–42. Richter, Cedric, et al. “Off-the-Shelf Cooperative Software Verification by Splitting Programs Dynamically.” Software Engineering 2026, vol. P-377, Gesellschaft für Informatik, 2026, pp. 41–42, doi:<a href="https://doi.org/10.18420/se2026_45">10.18420/se2026_45</a>. Richter, Cedric, Marek Chalupa, Marie Christine Jakobs, and Heike Wehrheim. “Off-the-Shelf Cooperative Software Verification by Splitting Programs Dynamically.” In Software Engineering 2026, P-377:41–42. Gesellschaft für Informatik, 2026. <a href="https://doi.org/10.18420/se2026_45">https://doi.org/10.18420/se2026_45</a>. C. Richter, M. Chalupa, M.C. Jakobs, H. Wehrheim, in:, Software Engineering 2026, Gesellschaft für Informatik, 2026, pp. 41–42. Richter C, Chalupa M, Jakobs MC, Wehrheim H. 2026. Off-the-Shelf cooperative software verification by splitting programs dynamically. Software Engineering 2026. SE: Software Engineering, Lecture Notes in Informatics, vol. P-377, 41–42. Richter C, Chalupa M, Jakobs MC, Wehrheim H. Off-the-Shelf cooperative software verification by splitting programs dynamically. In: Software Engineering 2026. Vol P-377. Gesellschaft für Informatik; 2026:41-42. doi:<a href="https://doi.org/10.18420/se2026_45">10.18420/se2026_45</a> Richter, C., Chalupa, M., Jakobs, M. C., & Wehrheim, H. (2026). Off-the-Shelf cooperative software verification by splitting programs dynamically. In Software Engineering 2026 (Vol. P-377, pp. 41–42). Bonn, Switzerland: Gesellschaft für Informatik. <a href="https://doi.org/10.18420/se2026_45">https://doi.org/10.18420/se2026_45</a> 226222026-08-02T22:01:54Z2026-10-19T08:49:32Z