Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917752434851840 |
|---|---|
| author | Frenkel, Eden Chajed, Tej Padon, Oded Shoham, Sharon |
| author_facet | Frenkel, Eden Chajed, Tej Padon, Oded Shoham, Sharon |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2405_10308 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas Frenkel, Eden Chajed, Tej Padon, Oded Shoham, Sharon Logic in Computer Science 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. |
| title | Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2405.10308 |