Invariant inference via quantified separation
Abstract/Contents
- Abstract
- Quantified first-order formulas, often with quantifier alternations, are increasingly used in the verification of complex systems. While automated theorem provers for first-order logic are becoming more robust, until recently invariant inference tools that handle quantifiers were restricted to purely universal formulas. We define and analyze first-order quantified separators and their application to inferring quantified invariants with alternations. A separator for a given set of positively and negatively labeled structures is a formula that is true on positive structures and false on negative structures. We investigate the problem of finding a separator from the class of formulas in prenex normal form with a bounded number of quantifiers and show this problem is NP-complete by reduction to and from SAT. Based on this computational primitive, we present a new PDR/IC3-based algorithm for finding inductive invariants with quantifier alternations. We tackle scalability issues that arise due to the large search space of quantified invariants by combining a breadth-first search strategy and a new syntactic form for quantifier-free bodies. The breadth-first strategy prevents inductive generalization from getting stuck in regions of the search space that are expensive to search and focuses instead on lemmas that are easy to discover. The new syntactic form is well-suited to lemmas with quantifier alternations by allowing both limited conjunction and disjunction in the quantifier-free body, while carefully controlling the size of the search space. We evaluate both separation itself and our combined invariant inference algorithm on a benchmark of primarily distributed protocols, including complex Paxos variants. We demonstrate separation can be solved in practice, and that our inference algorithm can solve more of the most complicated examples than other state-of-the-art techniques.
Description
| Type of resource | text |
|---|---|
| Form | electronic resource; remote; computer; online resource |
| Extent | 1 online resource. |
| Place | California |
| Place | [Stanford, California] |
| Publisher | [Stanford University] |
| Copyright date | 2022; ©2022 |
| Publication date | 2021; 2021 |
| Issuance | monographic |
| Language | English |
Creators/Contributors
| Author | Koenig, Jason Richard |
|---|---|
| Degree supervisor | Aiken, Alexander |
| Thesis advisor | Aiken, Alexander |
| Thesis advisor | Barrett, Clark |
| Thesis advisor | Trippel, Caroline |
| Degree committee member | Barrett, Clark |
| Degree committee member | Trippel, Caroline |
| Associated with | Stanford University, Computer Science Department |
Subjects
| Genre | Theses |
|---|---|
| Genre | Text |
Bibliographic information
| Statement of responsibility | Jason Richard Koenig. |
|---|---|
| Note | Submitted to the Computer Science Department. |
| Thesis | Thesis Ph.D. Stanford University 2022. |
| Location | https://purl.stanford.edu/vx350kj7751 |
Access conditions
- Copyright
- © 2022 by Jason Richard Koenig
- License
- This work is licensed under a Creative Commons Attribution Non Commercial 3.0 Unported license (CC BY-NC).
Also listed in
Loading usage metrics...