TY - GEN
T1 - Pono
T2 - 33rd International Conference on Computer Aided Verification, CAV 2021
AU - Mann, Makai
AU - Irfan, Ahmed
AU - Lonsing, Florian
AU - Yang, Yahan
AU - Zhang, Hongce
AU - Brown, Kristopher
AU - Gupta, Aarti
AU - Barrett, Clark
N1 - Publisher Copyright:
© 2021, The Author(s).
PY - 2021
Y1 - 2021
N2 - Symbolic 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 Pono, an open-source SMT-based model checker. Pono 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, Pono prioritizes transparency (developed as an open-source project on GitHub), flexibility (Pono 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 Pono is competitive with state-of-the-art tools.
AB - Symbolic 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 Pono, an open-source SMT-based model checker. Pono 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, Pono prioritizes transparency (developed as an open-source project on GitHub), flexibility (Pono 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 Pono is competitive with state-of-the-art tools.
UR - http://www.scopus.com/inward/record.url?scp=85112139620&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85112139620&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-81688-9_22
DO - 10.1007/978-3-030-81688-9_22
M3 - Conference contribution
AN - SCOPUS:85112139620
SN - 9783030816872
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 461
EP - 474
BT - Computer Aided Verification - 33rd International Conference, CAV 2021, Proceedings
A2 - Silva, Alexandra
A2 - Leino, K. Rustan
PB - Springer Science and Business Media Deutschland GmbH
Y2 - 20 July 2021 through 23 July 2021
ER -