Pono: A Flexible and Extensible SMT-Based Model Checker
The work
| Authors | Makai Mann; Ahmed Irfan; Florian Lonsing; Yahan Yang; Hongce Zhang; Kristopher Brown; Aarti Gupta; Clark Barrett |
|---|---|
| Editors | |
| Type | incollection |
| Year | 2021 |
| Citekey | mann2021pono |
Where it appeared
| Published in | Computer Aided Verification |
|---|---|
| Publisher | Springer International Publishing |
| Series | Lecture Notes in Computer Science |
| Pages | 461--474 |
Identifiers
| DOI | 10.1007/978-3-030-81688-9_22 |
|---|---|
| ISSN | 0302-9743 |
| ISBN | 978-3-030-81687-2 |
Access
| Landing page | https://doi.org/10.1007/978-3-030-81688-9_22 |
|---|
From crossref.
Abstract
AbstractSymbolic model checking is an important tool for finding bugs (or proving the absence of bugs) in modern system designs. Because of this, improving the ease of use, scalability, and performance of model checking tools and algorithms continues to be an important research direction. In service of this goal, we present , an open-source SMT-based model checker. is designed to be both a research platform for developing and improving model checking algorithms, as well as a performance-competitive tool that can be used for academic and industry verification applications. In addition to performance, prioritizes transparency (developed as an open-source project on GitHub), flexibility ( can be adapted to a variety of tasks by exploiting its general SMT-based interface), and extensibility (it is easy to add new algorithms and new back-end solvers). In this paper, we describe the design of the tool with a focus on the flexible and extensible architecture, cover its current capabilities, and demonstrate that is competitive with state-of-the-art tools.
How it got here
| How it got here | agent via crossref |
|---|---|
| Added | 2026-10-26 05:51 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Filed under
Cite it as
@incollection{mann2021pono,
title = {Pono: A Flexible and Extensible SMT-Based Model Checker},
author = {Makai Mann and Ahmed Irfan and Florian Lonsing and Yahan Yang and Hongce Zhang and Kristopher Brown and Aarti Gupta and Clark Barrett},
year = {2021},
booktitle = {Computer Aided Verification},
publisher = {Springer International Publishing},
series = {Lecture Notes in Computer Science},
pages = {461--474},
isbn = {978-3-030-81687-2},
issn = {0302-9743},
doi = {10.1007/978-3-030-81688-9_22},
}
This record lives at https://refs.drheap.org/mann2021pono/ and will keep doing so.