论文标题
抽象归纳不变的可决定性和合成
Decidability and Synthesis of Abstract Inductive Invariants
论文作者
论文摘要
在给定域内不变的归纳不变的可决定性和综合在许多软件和硬件验证系统中起着重要作用。我们在这里考虑属于抽象域$ a $的归纳不变，即抽象解释中定义的，即确保在任何系统属性的$ a $ a $中存在最佳近似。在这种情况下，我们研究了$ a $ a $过渡系统中的抽象归纳不变性及其相应算法合成的可决定性。我们的模型依赖于一些一般结果，这些结果将抽象归纳不变的存在与最低固定点的最佳正确近似值相关联，在$ a $ a $ a $的转移函数及其完整性属性中。这种方法使我们能够为抽象感应不变剂得出可定义性和合成结果，该结果应用于众所周知的Kildall恒定传播和Karr的仿射平等性摘要域。此外，我们表明，在逻辑公式域中合成归纳不变性的最新一般算法可以从我们的结果系统地得出，并概括为计算抽象电感不变性的一系列算法。
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.
