For many decades, advances in static verification have focused on linear integer arithmetic (LIA) programs. Many real-world programs are, however, written with non-linear integer arithmetic (NLA) expressions, such as programs that model physical events, control systems, or nonlinear activation functions in neural networks. While there are some approaches to reasoning about such NLA programs, still many verification tools fall short when trying to analyze them. To expand the scope of existing tools, we introduce a new method of converting programs with NLA expressions into semantically equivalent LIA programs via a technique we call dual rewriting. Dual rewriting discovers a linear replacement for an NLA Boolean expression (e.g. as found in conditional branching), simultaneously exploring both the positive and negative side of the condition, and using a combination of static validation and dynamic generalization of counterexamples. While perhaps surprising at first, this is often possible because the truth value of a Boolean NLA expression can be characterized in terms of a Boolean combination of linearly-described regions/intervals where the expression is true and those where it is false. The upshot is that rewriting NLA expressions to LIA expressions beforehand enables off-the-shelf LIA tools to be applied to the wider class of NLA programs. We built a new tool DrNLA and show it can discover LIA replacements for a variety of NLA programs. We then applied our work to branching-time verification of NLA programs, creating the first set of such benchmarks (92 in total) and showing that DrNLA's rewriting enable tools such as FuncTion and T2 to verify CTL properties of 42 programs that previously could not be verified. We also show a potential use of DrNLA assisting Frama-C in program slicing, and report that execution speed is not impacted much by rewriting.

翻译：数十年来，静态验证的进展主要集中于线性整数算术（LIA）程序。然而，许多真实世界程序包含非线性整数算术（NLA）表达式，例如模拟物理事件、控制系统或神经网络中的非线性激活函数的程序。尽管存在一些处理NLA程序的推理方法，但许多验证工具在分析这类程序时仍显不足。为扩展现有工具的范围，我们提出一种新方法，通过名为"双重重写"的技术，将包含NLA表达式的程序转换为语义等价的LIA程序。双重重写通过同时探索条件正反两侧，结合静态验证与反例动态泛化，为NLA布尔表达式（如条件分支中的表达式）发现线性替代形式。这之所以可行（尽管初看令人惊讶），是因为布尔型NLA表达式的真值可通过线性描述的区域/区间的布尔组合来刻画——这些区域中表达式为真或为假。关键在于，预先将NLA表达式重写为LIA表达式，使得现成的LIA工具能够应用于更广泛的NLA程序类别。我们构建了新工具DrNLA，并展示了其为多种NLA程序发现LIA替代形式的能力。随后我们将工作应用于NLA程序的分支时间验证，创建了首批此类基准测试集（共92个），证明DrNLA的重写使FuncTion和T2等工具能够验证42个此前无法验证程序的CTL属性。我们还展示了DrNLA在辅助Frama-C进行程序切片中的潜在应用，并指出重写对执行速度影响甚微。