Empirically Scalable Invariant Generation Leveraging Divide-and-Conquer with Pruning

Invariant generation is a critical task in program verification. Literature highlights Farkas’ Lemma as a principal sound and complete framework for proactively generating tight invariants in constraint-solving. Recent advances have identified the conversion from CNF to DNF as a major bottleneck, leading to a combinatorial explosion. In this study, we introduce an optimized algorithm to address the combinatorial explosion by trading off space for time-efficiency. Our approach employs two key strategies to boost speed. First, we apply a divide-and-conquer strategy to decompose a complex problem into smaller, more manageable subproblems that can be solved quickly and in parallel. Second, we intelligently apply a pruning strategy in two ways, navigating the depth-first search process to avoid unnecessary checks. These improvements maintain the accuracy and speed up the analysis. The experiments indicate that our approach outperforms the state-of-the-art, demonstrating significant speed improvements. With this solution, we bring a significant advance in accelerating invariant generation with Farkas’ Lemma.