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.

翻译：本文为使用抽象解释与由量化一阶逻辑公式集合构成的抽象域提供了实践基础。该抽象域初看似乎不可行，因为涉及公式的复杂性以及公式集合（抽象元素）的庞大规模。我们提出了一种高效的抽象元素表示方法，基于一种新颖的语法包含关系来消除冗余，该关系在语义蕴涵上进行了下近似。我们开发了算法与数据结构，用于在抽象元素表示上高效计算抽象元素与具体状态抽象结果的并（join）。为验证该域的可行性，我们利用所提出的数据结构和算法实现了一个符号抽象算法，用于计算迁移系统的最优抽象变换子的最小不动点，这对应于最强的归纳不变量。我们成功地在与最先进的属性导向方法相当的时间内，找到了例如Paxos的最小不动点（在我们的表示中包含1438个具有forall-exists-forall量化的公式）。