AI 中文总结
针对程序分析中最佳归纳不变式综合的效率挑战，提出基于一阶理论量化约束优化的新公式及两种位向量程序算法，在基准测试中性能优于传统方法，可解决更多基准并提升高位宽下的扩展性与验证效果。
AI 中文摘要
综合最佳归纳不变式（BII）是程序分析与验证的基础，但现有方法面临显著的效率挑战。我们通过一阶理论中量化约束的数学优化视角，为该问题提出新的公式化方案，该方案为BII问题提供了构造性与可操作的视角，并开辟了新的算法途径。基于此公式，我们提出两种针对位向量程序的新算法：一种是利用格结构的策略引导线性搜索，另一种是按从高位到低位解析绑定位的逐位贪心方法，其求解器调用次数与位宽呈线性关系。我们在一套全面的基准测试集上评估了所提方法，结果显示其相较于基于符号抽象与混沌迭代的传统方法，性能有显著提升。实验表明，所提方法比基线方法多解决高达86%的基准测试，且在高位宽下求解器调用次数的扩展性更好，与k-归纳结合时验证有效性也得到提升。
英文摘要
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.
