SMPT: A Testbed for Reachability Methods in Generalized Petri Nets
arXiv:2302.14741 · doi:10.1007/978-3-031-27481-7_25
Abstract
SMPT (for Satisfiability Modulo Petri Net) is a model checker for reachability problems in Petri nets. It started as a portfolio of methods to experiment with symbolic model checking, and was designed to be easily extended. Some distinctive features are its ability to benefit from structural reductions and to generate verdict certificates. Our tool is quite mature and performed well compared to other state-of-the-art tools in the Model Checking Contest.
FM 2023 - 25th International Symposium on Formal Methods,, Mar 2023, L{ü}beck, Germany