publications

2026

1. TASE

   Unleash the Hidden Power of CAR-Based Model Checking Through Dynamic Traversal

   Yibo Dong, Yu Chen, Jianwen Li, and Geguang Pu

   In Theoretical Aspects of Software Engineering, 2026

   Abs

   Complementary Approximate Reachability (CAR) is a leading SAT-based model checking algorithm that combines under- and over-approximating state sequences to verify safety properties. However, its performance is hindered by redundant computations caused by the fixed-order traversal of the under-approximating sequence. To address such a limit, in this paper, we propose a dynamic traversal strategy to optimize CAR. By identifying common inefficiency patterns, we introduce heuristic methods and a scoring mechanism to prioritize states that are more likely to advance verification. We also prove that the correctness of the CAR algorithm can be preserved while exploring only a subset of the U-sequence, enabling partial traversal strategies that significantly reduce computational overhead. Experimental results demonstrate that our approach could solve 10% more cases than the previous best CAR implementation [17] and outperform state-of-the-art IC3 model checkers, e.g., IC3-REF [4, 11]. Our method bridges the gap between CAR’s theoretical potential and practical scalability, offering a more efficient solution for industrial-scale verification.

2025

1. IEEE-TCAD

   Revisiting Assumptions Ordering in CAR-Based Model Checking

   Yibo Dong, Yu Chen, Jianwen Li, Geguang Pu, and Ofer Strichman

   IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2025

   DOI
2. SPIN

   Accelerating CAR-based Model-Checking with Multiple Unsatisfiable Cores

   Yibo Dong, Xiwei Wu, Jianwen Li, Geguang Pu, and Ofer Strichman

   2025

2023

1. ESEC/FSE

   LightF3: A Lightweight Fully-Process Formal Framework for Automated Verifying Railway Interlocking Systems

   Yibo Dong, Xiaoyu Zhang, Yicong Xu, Chang Cai, Yu Chen, and 3 more authors

   In Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, San Francisco, CA, USA, 2023

   Abs DOI

   Interlocking has long played a crucial role in railway systems. Its functional correctness, particularly concerning safety, forms the foundation of the entire signaling system. To date, numerous efforts have been made to formally model and verify interlocking systems. However, two main problems persist in most prior work: (1) The formal description of the interlocking system heavily depends on reusing existing models, which often results in overgeneralization and failing to fully utilize the intrinsic characteristics of interlocking systems. (2) The verification techniques of current approaches may quickly become outdated, and there is no adaptable method to integrate state-of-the-art verification algorithms or tools. To address the above issues, we present LightF3, a lightweight and fully-process formal framework for modeling and verifying railway interlocking systems. LightF3 provides RIS-FL, a formal language based on FQLTL (a variant of LTL) to model the system and its specifications. LightF3 transforms the RIS-FL model automatically to the aiger model, which is the mainstream input of state-of-the-art model checkers, and then invokes the most advanced checkers to complete the verification task. We evaluated LightF3 by testing five real station instances from our industrial partner, demonstrating its effectiveness as a new framework. Additionally, we analyzed the statistics of the verification results from different model-checking techniques, providing useful conclusions for both the railway interlocking and formal methods communities.