“Pono 2.0: A Versatile SMT-Based Model Checker for Safety and Liveness (Long Tool Paper)” by Aron Ricardo Perez{-}Lopez, Po{-}Chun Chien, Florian Lonsing, Samantha Archer, Ahmed Irfan, and Clark W. Barrett. In Formal Methods - 27th International Symposium, FM 2026, Tokyo, Japan, May 18-22, 2026, Proceedings, Part II, (Augusto Sampaio and Marielle Stoelinga, eds.), May 2026, pp. 3-26.
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.
BibTeX entry:
@inproceedings{PCL+26,
author = {Aron Ricardo Perez{-}Lopez and Po{-}Chun Chien and Florian
Lonsing and Samantha Archer and Ahmed Irfan and Clark W. Barrett},
editor = {Augusto Sampaio and Marielle Stoelinga},
title = {Pono 2.0: {A} Versatile SMT-Based Model Checker for Safety and
Liveness (Long Tool Paper)},
booktitle = {Formal Methods - 27th International Symposium, {FM} 2026,
Tokyo, Japan, May 18-22, 2026, Proceedings, Part {II}},
series = {Lecture Notes in Computer Science},
pages = {3--26},
publisher = {Springer},
month = may,
year = {2026},
doi = {10.1007/978-3-032-26220-2_1},
url = {https://doi.org/10.1007/978-3-032-26220-2_1}
}
(This webpage was created with bibtex2web.)