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

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.