|
|
|
|
|
|
|
| SPIN | Bell Labs | free | Promella (process algebra) | Inline assertions, end-state labels, progress-state labels, acceptance-state labels, LTL properties, or never-claims (Buchi automata) | |
| nuSMV (the new Symbolic Model Verifier) | Carnegie Mellon University , Group at University of Genova
Mechanized Reasoning Group at University of Trento. |
free | SMV-like language (for Kripke structure) | LTL, CTL | faster then SMV, require more memory, better documented |
| BMC (bounded model checker Early beta version) | Carnegie Mellon | free | Simple SMV-like language (no modules). | Uses SAT procedures instead of BDDs:
bounded depth but usually faster, less memory. |
|
| MCB (a non symbolic model checker) | Carnegie Mellon | free | Moore FSM | CTL | |
| Fc2Tools
& Autograph (graphic editor)
Inria |
Inria and Ecole des Mines | free | Communication automata (process algebra), | observers or modal temporal logic formulae | |
| Verisoft | Lucent (Bell Labs) | free | Any program | ||
| SGM (state graph manipulator) | Chung Cheng University
(Taiwan) |
free for education / research | Timed automata | model checking is under development | |
| EVALUATOR (CADP) | Inria | free for research | LTS, there are interfaces/on fly translators for Lotos, IF, XTL, experimental translators from UML etc | regular alternation-free mu-calculus with Boolean formulas over actions and regular expressions over action sequences. Facilities for building property libraries | a part of CADP package |
Model checker list
http://www.abo.fi/~johan.lilius/mc/mclinks.html
FSM tool lists
http://www.csd.uwo.ca/staff/drraymon/.grail/links.html
http://www-ihs.theoinf.tu-ilmenau.de/forschung/links/fsm-tools.html
Some tools for Discrete Mathematics (graphs, posets etc)