P-IC3: Racing Three IC3 Workers with Different Literal-Deletion Orders

Abstract

Parallel portfolios provide a practical means of exploiting the behavioral diversity of IC3/PDR heuristics. Building on the observation that different literal-deletion orders can lead to different generalized clauses and verification trajectories, we present P-IC3, a parallel portfolio that runs multiple deletion strategies concurrently. P-IC3 races three IC3 workers, each using IC3’s native deletion order, lexicographic ascending order, or lexicographic descending order, respectively, and returns the first conclusive result. This lightweight design exploits the complementary behavior induced by different literal-ordering policies while preserving the underlying IC3 proof rules and checks. We implement P-IC3 in Kind2 3.0.0 and evaluate its effectiveness on Lustre programs. The experimental results indicate that P-IC3 improves both verification coverage and response time. Under a 300-second timeout, P-IC3 solves 818 instances, including 20 missed by the single-worker Kind2-IC3 baseline, and achieves a 1.73× cumulative wall-clock speedup on their 798 common solves. The native, ascending, and descending workers finish first on 197, 304, and 317 instances, respectively, indicating that each order can be advantageous on different instances. Compared with racing three identical native workers (Base×3), P-IC3 solves 14 more instances and achieves a 1.50× speedup on their 802 common solves. This comparison suggests that deletion-order diversity offers benefits beyond those attributable to parallel execution alone.

Guangyu (Gary) Hu

Researcher at Huawei Hong Kong Research Center, Fermat Lab

My research interests include LLM + formal verification reasoning and hardware formal verification.