简洁表示控制流图的策略迭代不变量生成
Invariant Generation through Strategy Iteration in Succinctly Represented Control Flow Graphs
摘要：
我们考虑的问题计算数值不变的程序，例如边界上的数值程序变量的值。更具体地说，我们研究的问题进行静态分析的抽象解释使用模板线性约束域。这样的不变量可以通过Kleene迭代获得，为了保证终止，通过加宽算子加速。然而，在许多情况下，应用这种形式的外推导致不变量比可以在使用中的抽象域中表达的最强归纳不变量弱。传统抽象解释技术的另一个众所周知的不精确性来源源于它们在控制流图中的合并节点处使用连接运算符。所提到的弱点可能阻止这些方法证明安全特性。我们在本文中开发的技术解决了这两个问题：与通过加宽算子加速的Kleene迭代相反，它保证产生可以在使用的模板线性约束域中表达的最强归纳不变量。它还通过区分无循环代码段的所有路径来避免连接运算符。从形式上讲，我们的技术计算的最小不动点在一个给定的模板线性约束域的过渡关系，简洁地表示为存在量化的线性实数算术公式。与以前发表的依赖于量词消去的技术相比，我们的算法被证明具有最佳的复杂性：我们证明了与我们的不动点问题相关联的决策问题是在多项式时间层次的第二层。
英文摘要：
We consider the problem of computing numerical invariants of programs, for instance bounds on the values of numerical program variables. More specifically, we study the problem of performing static analysis by abstract interpretation using template linear constraint domains. Such invariants can be obtained by Kleene iterations that are, in order to guarantee termination, accelerated by widening operators. In many cases, however, applying this form of extrapolation leads to invariants that are weaker than the strongest inductive invariant that can be expressed within the abstract domain in use. Another well-known source of imprecision of traditional abstract interpretation techniques stems from their use of join operators at merge nodes in the control flow graph. The mentioned weaknesses may prevent these methods from proving safety properties. The technique we develop in this article addresses both of these issues: contrary to Kleene iterations accelerated by widening operators, it is guaranteed to yield the strongest inductive invariant that can be expressed within the template linear constraint domain in use. It also eschews join operators by distinguishing all paths of loop-free code segments. Formally speaking, our technique computes the least fixpoint within a given template linear constraint domain of a transition relation that is succinctly expressed as an existentially quantified linear real arithmetic formula. In contrast to previously published techniques that rely on quantifier elimination, our algorithm is proved to have optimal complexity: we prove that the decision problem associated with our fixpoint problem is in the second level of the polynomial-time hierarchy.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
