SMPT: A Testbed for Reachability Methods in Generalized Petri Nets

Nicolas Amat, Silvano Dal Zilio
In FM 2023 — 25th International Symposium on Formal Methods, mar 2023.

 DOI〈10.1007/978-3-031-27481-7_25〉  HAL-04007410

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.

Citation

#

@InProceedings{DalzilioS:fm2023smpt,
   author    = {Amat, Nicolas and {Dal Zilio}, Silvano},
   title     = {{SMPT: A Testbed for Reachability Methods in Generalized Petri Nets}},
   booktitle = {FM 2023 -- 25th International Symposium on Formal Methods},
   series    = {Lecture Notes in Computer Science},
   volume    = {14000},
   publisher = {Springer-Verlag},
   doi = {10.1007/978-3-031-27481-7_25},
   pages     = {445--453},
   month     = mar, 
   year      = 2023
}