Tools:

• Bomotest is a formal conformance testing tool for the ioco-conformance. It uses labeled 1-bounded Petri nets as its specification model, and employs specification coverage based test selection heuristic incorporating bounded model checking algorithms. This is joint work with Tuomo Pyhälä.
• boundsmodels is a bounded LTL-X model checker which generates logic programs with stable model semantics from 1-bounded Petri nets. It supports step and interleaving semantics.
• punroll is a bounded reachability checker which generates constrained Boolean circuits from 1-bounded Petri nets. It supports process, step, and interleaving semantics.
• unfsmodels is an LTL-X model checker with net unfoldings.
• mcsmodels is a deadlock and reachability checker using finite complete prefixes generated by the PEP tool from 1-bounded Petri nets. It uses the smodels constraint-based logic programming system as its computational engine.
• PROD is a reachability analyzer for Pr/T-nets with advanced features such as : stubborn sets, sleep sets, on-the-fly tester based verification, on-the-fly LTL model checking, CTL model checking. The main authon of PROD is Kimmo Varpaaniemi, I just implemented the CTL model checking part.
• dlsmodels is an older version of mcsmodels limited to deadlock checking only.