Augmenting transition systems for scalable symbolic model checking
Abstract/Contents
- Abstract
- Symbolic model checking is an important tool for finding bugs (or proving the absence of bugs) in modern hardware and software systems. Because of this, improving the ease of use, scalability, and performance of model checking tools and algorithms continues to be an influential research direction. In service of this goal, we present two tools followed by two novel techniques that expand the state of the art in symbolic model checking. The first tool, Smt-Switch, provides simple, uniform, and high-performance access to satisfiability modulo theories (SMT) solving for applications in areas such as automated reasoning, planning, and formal verification. We then present Pono, an open-source SMT-based model checker built on Smt-Switch. Pono is designed to be both a research platform for developing and improving model checking algorithms, as well as a performance-competitive tool to be used for academic and industry verification applications. Next, we use this infrastructure to prototype two model checking approaches that reduce the difficulty of a problem by modifying the given transition system model. First, we develop a framework for model checking infinite-state systems by automatically augmenting them with auxiliary variables, enabling quantifier-free induction proofs for systems that would otherwise require quantified invariants. We combine this mechanism with a counterexample-guided abstraction refinement scheme for the theory of arrays. Our approach can, in many cases, reduce inductive reasoning with quantifiers and arrays to quantifier-free and array-free reasoning. Second, we adapt partial order reduction (POR) for bounded model checking of synchronous hardware and introduce a novel technique that makes partial order reduction practical in this new domain. We demonstrate substantial performance improvements over unaltered bounded model checking with this technique, despite the conventional wisdom that POR is only applicable for asynchronous systems.
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 | 2021; ©2021 |
| Publication date | 2021; 2021 |
| Issuance | monographic |
| Language | English |
Creators/Contributors
| Author | Mann, Makai Michael |
|---|---|
| Degree supervisor | Barrett, Clark |
| Thesis advisor | Barrett, Clark |
| Thesis advisor | Horowitz, Mark (Mark Alan) |
| Thesis advisor | Matthews, John |
| Thesis advisor | Trippel, Caroline |
| Degree committee member | Horowitz, Mark (Mark Alan) |
| Degree committee member | Matthews, John |
| Degree committee member | Trippel, Caroline |
| Associated with | Stanford University, Department of Electrical Engineering |
Subjects
| Genre | Theses |
|---|---|
| Genre | Text |
Bibliographic information
| Statement of responsibility | Makai Mann. |
|---|---|
| Note | Submitted to the Department of Electrical Engineering. |
| Thesis | Thesis Ph.D. Stanford University 2021. |
| Location | https://purl.stanford.edu/mn350tb8500 |
Access conditions
- Copyright
- © 2021 by Makai Michael Mann
- 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...