抽象归纳不变量的可判定性与综合
Decidability and Synthesis of Abstract Inductive Invariants
摘要：
在许多软件和硬件验证系统中，在给定域范围内的归纳不变量的可判定性和综合起着重要的作用。我们认为在这里归纳不变量属于一个抽象域$A$的定义在抽象的解释，即，确保存在的最佳逼近$A$的任何系统属性。在这种情况下，我们研究的可判定性存在的抽象归纳不变量的$A$的过渡系统和相应的算法合成。我们的模型依赖于一些一般性的结果，这些结果将抽象归纳不变量的存在性与过渡系统的传递函数的$A$中的最佳正确逼近的最小不动点及其完备性联系起来。这种方法使我们能够推导出可判定性和合成结果的抽象归纳不变量，适用于著名的基尔达尔的常数传播和卡尔的仿射等式抽象域。此外，我们表明，最近的一般算法合成归纳不变量域的逻辑公式，可以系统地从我们的结果和推广到一系列的算法计算抽象归纳不变量。
英文摘要：
Decidability and synthesis of inductive invariants ranging in a given domain play an important role in many software and hardware verification systems. We consider here inductive invariants belonging to an abstract domain $A$ as defined in abstract interpretation, namely, ensuring the existence of the best approximation in $A$ of any system property. In this setting, we study the decidability of the existence of abstract inductive invariants in $A$ of transition systems and their corresponding algorithmic synthesis. Our model relies on some general results which relate the existence of abstract inductive invariants with least fixed points of best correct approximations in $A$ of the transfer functions of transition systems and their completeness properties. This approach allows us to derive decidability and synthesis results for abstract inductive invariants which are applied to the well-known Kildall's constant propagation and Karr's affine equalities abstract domains. Moreover, we show that a recent general algorithm for synthesizing inductive invariants in domains of logical formulae can be systematically derived from our results and generalized to a range of algorithms for computing abstract inductive invariants.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
