一句话：提出动态程序切分 DPS，使协作验证按需拆分程序并调度多个验证器，解决单个验证器无法完成的任务。
协作软件验证通过让多个验证工具分工来提高验证效率与效果，但现有方法常采用静态分解且使用专有格式，难以利用现成验证器。本文提出动态程序切分（DPS）：验证从将任务交给验证器 V1 开始；当 V1 认为当前任务难以验证时，按需把程序拆分为子任务并重启验证。该过程在发现违例、所有子任务完成或满足用户停止条件时结束；若触发停止条件，则把未完成子任务合并后交给下一个验证器 V2，并重复此流程。这样，分解由具体验证器的验证难度驱动，可发挥验证器之间的互补优势。作者实现了 DPS，并在 SV-COMP 基准上评估，表明其能解决所有组成验证器单独无法解决的任务，且没有显著额外开销。
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$V_{1}$. Whenever$V_{1}$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$V_{2}$, 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.
DOI 原文 ·
@inproceedings{paperbot8819,
title = {Cooperative Software Verification via Dynamic Program Splitting},
author = {Cedric Richter and Marek Chalupa and Marie-Christine Jakobs and Heike Wehrheim},
booktitle = {ICSE},
year = {2025},
doi = {10.1109/icse55347.2025.00092}
}