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^*$量词的公式）找到了最小不动点。