The Center for Advanced Distributed System Engineering Group at the School of Computing and Information Sciences at FIU
Free Counter
A tool that leverages a SMT solver Z3 to verify formal models in High-level Petri nets. The tool automatically abstracts model’s states and verification properties into a subset of first-order logic formula, run Z3 to check the formula’s satisfiability and then analyze the checking result. Compare to traditional model checking, it reduces the searching state space but increases computing times.
The current version of PIPE+Verifier source code can be downloaded at here PIPE+
The related paper: "Su Liu, Reng Zeng, Zhuo Sun, Xudong He, Bounded Model Checking High Level Petri Nets in PIPE+Verifier ."