ISSTA 2025
Wed 25 - Sat 28 June 2025 Trondheim, Norway
co-located with FSE 2025
Wed 25 Jun 2025 16:00 - 16:25 at Aurora C - Formal Analysis and Symbolic Execution Chair(s): Na Meng

Recently, model checking guided testing (MCGT) approaches have been proposed to systematically test distributed systems. MCGT automatically generates test cases by traversing the entire verified abstract state space derived from a distributed system’s formal specification, and it checks whether the target system behaves correctly during testing. Despite the effectiveness of MCGT, testing a distributed system with MCGT is often costly and can take weeks to complete. This inefficiency is exacerbated when distributed systems evolve, such as when new features are introduced or bugs are fixed. We must re-run the entire testing process for the evolved system to ensure its correctness, rendering MCGT not only resource-intensive but also inefficient. To reduce the overhead of model checking guided testing during distributed system evolution, we propose iMocket, a novel model checking guided incremental testing approach for distributed systems. We first extract the changes from both the formal specification and system implementation. We then identify the affected states within the abstract state space and generate incremental test cases that specifically target these states, thereby avoiding redundant testing of unaffected states. We evaluate iMocket using 12 real-world change scenarios drawn from three popular distributed systems. The experimental results demonstrate that iMocket can reduce the number of test cases by 74.83%, highlighting its effectiveness in lowering testing costs for distributed systems.

Wed 25 Jun

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 17:30
Formal Analysis and Symbolic ExecutionResearch Papers / Tool Demonstrations at Aurora C
Chair(s): Na Meng Virginia Tech
16:00
25m
Talk
Model Checking Guided Incremental Testing for Distributed Systems
Research Papers
Yu Gao Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Dong Wang Institute of software, Chinese academy of sciences, Wensheng Dou Institute of Software Chinese Academy of Sciences, Wenhan Feng Institute of Software, Chinese Academy of Sciences, Yu Liang Institute of Software Chinese Academy of Sciences, Yuan Feng Wuhan Dameng Database Co., Ltd, Jun Wei Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences
DOI
16:25
25m
Talk
Identifying Multi-Parameter Constraint Errors in Python Data Science Library API Documentations
Research Papers
Xiufeng Xu Nanyang Technological University, Fuman Xie University of Queensland, Chenguang Zhu Meta AI, Guangdong Bai University of Queensland, Sarfraz Khurshid University of Texas at Austin, Yi Li Nanyang Technological University
DOI Pre-print
16:50
25m
Talk
Freesia: Verifying Correctness of TEE Communication with Concurrent Separation Logic
Research Papers
Fanlang Zeng Zhejiang University, Rui Chang Zhejiang University, Hongjian Liu Zhejiang University, Hangzhou, China
DOI
17:15
15m
Demonstration
TBFV4J: An Automated Testing-Based Formal Verification Tool for Java
Tool Demonstrations

Information for Participants
Wed 25 Jun 2025 16:00 - 17:30 at Aurora C - Formal Analysis and Symbolic Execution Chair(s): Na Meng
Info for room Aurora C:

Aurora C is the third room in the Aurora wing.

When facing the main Cosmos Hall, access to the Aurora wing is on the right, close to the side entrance of the hotel.

:
:
:
: