Search papers, labs, and topics across Lattice.
This paper addresses the inefficiencies in synthesizing best inductive invariants (BII) for program analysis by reformulating the problem as a mathematical optimization challenge over quantified constraints in first-order theories. The authors introduce two novel algorithms tailored for bit-vector programs: a strategically guided linear search leveraging lattice structures and a bitwise greedy method that efficiently resolves bound bits. Experimental evaluations reveal that these approaches solve up to 86% more benchmarks than traditional methods, showcasing enhanced scalability and verification effectiveness, particularly in high bit-width scenarios.
A new optimization-based approach to inductive invariant synthesis achieves an 86% increase in benchmark solvability compared to traditional methods.
Synthesizing best inductive invariants (BII) is fundamental to program analysis and verification, yet existing approaches face significant efficiency challenges. We introduce a new formulation for the problem through the lens of mathematical optimization over quantified constraints in first-order theories. The formulation offers a constructive and operational perspective on the BII problem and opens new algorithmic avenues. Building on this formulation, we present two new algorithms for bit-vector programs: a strategically guided linear search that exploits the lattice structure and a bitwise greedy approach that resolves bound bits from high to low with a solver-call count linear in bit-width. We evaluate our approach on a comprehensive benchmark suite, demonstrating significant performance improvements over conventional methods based on symbolic abstraction and chaotic iteration. Experimental results demonstrate our approach solves up to 86\% more benchmarks than baseline methods, with improved scaling in solver-call count for high bit-widths and improved verification effectiveness when integrated with k-induction.
