This paper lays a practical foundation for using abstract interpretation with an abstract domain that consists of sets of quantified first-order logic formulas. This abstract domain seems infeasible at first sight due to the complexity of the formulas involved and the enormous size of sets of formulas (abstract elements). We introduce an efficient representation of abstract elements, which eliminates redundancies based on a novel syntactic subsumption relation that under-approximates semantic entailment. We develop algorithms and data structures to efficiently compute the join of an abstract element with the abstraction of a concrete state, operating on the representation of abstract elements. To demonstrate feasibility of the domain, we use our data structures and algorithms to implement a symbolic abstraction algorithm that computes the least fixpoint of the best abstract transformer of a transition system, which corresponds to the strongest inductive invariant. We succeed at finding, for example, the least fixpoint for Paxos (which in our representation has 1,438 formulas with $\forall^*\exists^*\forall^*$ quantification) in time comparable to state-of-the-art property-directed approaches.

翻译：本文为使用抽象解释方法处理由一阶量化逻辑公式集合构成的抽象域奠定了实践基础。该抽象域初看起来难以实现，原因在于所涉及的公式结构复杂且公式集合（抽象元素）规模庞大。我们提出了一种高效的抽象元素表示方法，通过一种新颖的语法蕴含关系来消除冗余，该关系在语义蕴含的下近似意义上成立。我们开发了相应的算法与数据结构，能在抽象元素表示的基础上高效计算抽象元素与具体状态抽象结果之间的并运算。为证明该抽象域的可行性，我们利用所提出的数据结构与算法实现了一个符号抽象算法，该算法可计算转移系统的最佳抽象变换子的最小不动点，对应最强归纳不变量。例如，我们成功为Paxos协议找到了最小不动点（在我们的表示中包含1,438个形如$\forall^*\exists^*\forall^*$量词前缀的公式），其计算时间与当前最先进的面向属性的方法相当。