---
OA_type: closed access
_id: '20024'
abstract:
- lang: eng
  text: '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.'
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.
article_processing_charge: No
author:
- first_name: Cedric
  full_name: Richter, Cedric
  last_name: Richter
- first_name: Marek
  full_name: Chalupa, Marek
  id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
  last_name: Chalupa
- first_name: Marie-Christine
  full_name: Jakobs, Marie-Christine
  last_name: Jakobs
- first_name: Heike
  full_name: Wehrheim, Heike
  last_name: Wehrheim
citation:
  ama: 'Richter C, Chalupa M, Jakobs M-C, Wehrheim H. Cooperative software verification
    via dynamic program splitting. In: <i>47th International Conference on Software
    Engineering</i>. IEEE; 2025:2087-2099. doi:<a href="https://doi.org/10.1109/ICSE55347.2025.00092">10.1109/ICSE55347.2025.00092</a>'
  apa: 'Richter, C., Chalupa, M., Jakobs, M.-C., &#38; Wehrheim, H. (2025). Cooperative
    software verification via dynamic program splitting. In <i>47th International
    Conference on Software Engineering</i> (pp. 2087–2099). Ottawa, ON, Canada: IEEE.
    <a href="https://doi.org/10.1109/ICSE55347.2025.00092">https://doi.org/10.1109/ICSE55347.2025.00092</a>'
  chicago: Richter, Cedric, Marek Chalupa, Marie-Christine Jakobs, and Heike Wehrheim.
    “Cooperative Software Verification via Dynamic Program Splitting.” In <i>47th
    International Conference on Software Engineering</i>, 2087–99. IEEE, 2025. <a
    href="https://doi.org/10.1109/ICSE55347.2025.00092">https://doi.org/10.1109/ICSE55347.2025.00092</a>.
  ieee: C. Richter, M. Chalupa, M.-C. Jakobs, and H. Wehrheim, “Cooperative software
    verification via dynamic program splitting,” in <i>47th International Conference
    on Software Engineering</i>, Ottawa, ON, Canada, 2025, pp. 2087–2099.
  ista: '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.'
  mla: Richter, Cedric, et al. “Cooperative Software Verification via Dynamic Program
    Splitting.” <i>47th International Conference on Software Engineering</i>, IEEE,
    2025, pp. 2087–99, doi:<a href="https://doi.org/10.1109/ICSE55347.2025.00092">10.1109/ICSE55347.2025.00092</a>.
  short: C. Richter, M. Chalupa, M.-C. Jakobs, H. Wehrheim, in:, 47th International
    Conference on Software Engineering, IEEE, 2025, pp. 2087–2099.
conference:
  end_date: 2025-05-06
  location: Ottawa, ON, Canada
  name: 'ICSE: International Conference on Software Engineering'
  start_date: 2025-04-26
corr_author: '1'
date_created: 2025-07-16T11:32:29Z
date_published: 2025-05-01T00:00:00Z
date_updated: 2025-09-30T14:01:55Z
day: '01'
department:
- _id: ToHe
doi: 10.1109/ICSE55347.2025.00092
ec_funded: 1
external_id:
  isi:
  - '001538318100163'
isi: 1
language:
- iso: eng
month: '05'
oa_version: None
page: 2087-2099
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
  call_identifier: H2020
  grant_number: '101020093'
  name: Vigilant Algorithmic Monitoring of Software
publication: 47th International Conference on Software Engineering
publication_identifier:
  eissn:
  - 1558-1225
  isbn:
  - '9798331505691'
publication_status: published
publisher: IEEE
quality_controlled: '1'
scopus_import: '1'
status: public
title: Cooperative software verification via dynamic program splitting
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
year: '2025'
...