TCSE logo 
 Sigsoft logo
Sustainability badge

This program is tentative and subject to change.

Fri 2 May 2025 11:15 - 11:30 at 210 - Security and Analysis 2

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 facts 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 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.

This program is tentative and subject to change.

Fri 2 May

Displayed time zone: Eastern Time (US & Canada) change

11:00 - 12:30
Security and Analysis 2Research Track at 210
11:00
15m
Talk
A Study of Undefined Behavior Across Foreign Function Boundaries in Rust Libraries
Research Track
Ian McCormack Carnegie Mellon University, Joshua Sunshine Carnegie Mellon University, Jonathan Aldrich Carnegie Mellon University
Pre-print
11:15
15m
Talk
Cooperative Software Verification via Dynamic Program Splitting
Research Track
Cedric Richter University of Oldenburg, Marek Chalupa Institute of Science and Technology Austria, Marie-Christine Jakobs LMU Munich, Germany, Heike Wehrheim University of Oldenburg
11:30
15m
Talk
Exposing the Hidden Layer: Software Repositories in the Service of SEO Manipulation
Research Track
Mengying Wu Fudan University, Geng Hong Fudan University, Wuyuao Mai Fudan University, Xinyi Wu Fudan University, Lei Zhang Fudan University, Yingyuan Pu QI-ANXIN Technology Research Institute, Huajun Chai QI-ANXIN Technology Research Institute, Lingyun Ying Qi An Xin Group Corp., Haixin Duan Institute for Network Science and Cyberspace, Tsinghua University; Qi An Xin Group Corp., Min Yang Fudan University
11:45
15m
Talk
Hetrify: Efficient Verification of Heterogeneous Programs on RISC-VAward Winner
Research Track
Yiwei Li School of Computer, National Univer sity of Defense Technology, Liangze Yin School of Computer, National Univer sity of Defense Technology, Wei Dong National University of Defense Technology, Jiaxin Liu National University of Defense Technology, Yanfeng Hu School of Computer, National Univer sity of Defense Technology, Shanshan Li National University of Defense Technology
12:00
15m
Talk
Hyperion: Unveiling DApp Inconsistencies using LLM and Dataflow-Guided Symbolic Execution
Research Track
Shuo Yang Sun Yat-sen University, Xingwei Lin Ant Group, Jiachi Chen Sun Yat-sen University, Qingyuan Zhong Sun Yat-sen University, Lei Xiao Sun Yat-sen University, renke huang Sun Yat-sen University, Yanlin Wang Sun Yat-sen University, Zibin Zheng Sun Yat-sen University
12:15
15m
Talk
SmartReco: Detecting Read-Only Reentrancy via Fine-Grained Cross-DApp Analysis
Research Track
Jingwen Zhang School of Software Engineering, Sun Yat sen University, Zibin Zheng Sun Yat-sen University, Yuhong Nan Sun Yat-sen University, Mingxi Ye Sun Yat-sen University, Kaiwen Ning Sun Yat-sen University, Yu Zhang Harbin Institute of Technology, Weizhe Zhang Harbin Institute of Technology
:
:
:
: