In: O. Grumberg (Ed.), Computer Aided Verification: 9th International Conference, CAV'97, Haifa, Israel, June 22-25, 1997, Proceedings, pages 472-475. June 1997.
Abstract: PROD is a reachability analyzer for Predicate/Transition nets. The tool incorporates several advanced reduced reachability graph generation methods. The tool also includes a CTL model checker and supports on-the-fly verification of LTL formulas. PROD is being used in industrial projects at the Digital Systems Laboratory.
Keywords: reachability analysis; verification; model checking; stubborn sets; Petri nets.