Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas

TL;DR

This paper presents a practical method for efficiently implementing an abstract domain of quantified first-order formulas, enabling effective symbolic analysis of complex systems like Paxos.

Contribution

It introduces a novel syntactic subsumption relation and algorithms that make the analysis of quantified formulas computationally feasible.

Findings

Successfully computed the least fixpoint for Paxos with complex quantification

Achieved performance comparable to state-of-the-art approaches

Demonstrated the domain's practicality for real-world systems

Abstract

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.