Circal
 University of South Australia
 ?
 XCircal
 Finitestate transition systems
 ?
 (1) Explicit
(2) OBDDbased

Concurrency Factory
 SUNY at Stony Brook, NC State University
 C++
 VPL (compiled into Facile)
 Finitestate transition systems
 Lineartime alternationfree modal mucalculus
 Explicit

Edinburgh Concurrency Workbench
 University of Edinburgh
 Standard ML
 CCS
 Finitestate transition systems
 Modal mucalculus
 Explicit

FC2Tools
 INRIA, Ecole des Mines
 ?
 Process algebra
 Finitestate transition systems
 ?
 ?

FDR2
 Formal Systems Design and Development Inc.
 ?
 CSP
 Finitestate transition systems
 ?
 Symbolic, onthefly

HyTech
 University of Berkeley
 C++
 Linear hybrid automata
 ?
 ICTL
 Symbolic, regionbased

JACK Tool Set
 University of Pisa
 Several
 Transition systems
 ?
 ACTL
 ?

Kronos
 VERIMAG
 ?
 Timed automata
 ?
 TCTL
 Symbolic, constraintbased

Mobility Workbench
 Universities of Edinburgh and Uppsala
 Standard ML
 Picalculus
 Transition systems
 (only equivalence checking)
 Explicit, onthefly

ModelChecking Kit
 Technical University of Munich
 Several
 Communicating automata, Petri nets
 Transition systems
 LTL, CTL
 Symbolic

North Carolina Concurrency Workbench
 North Carolina State University
 Standard ML
 Several process algebras
(Process Algebra Compiler)
 Finitestate transition systems
 Modal mucalculus
 Explicit

PEP
 University of Hildesheim
 C++
 Various (programs, automata, process algebras, nets)
 Petri nets
 CTL, LTL
 by Esparza

SGM
 Academia Sinica, Taiwan
 ?
 State graphs
 Transition systems
 ?
 ?

SMV
 CarnegieMellon University
 ?
 Automaton
 Finitestate transition systems
 CTL
 Symbolic, OBDDbased

SPIN
 Bell Laboratories
 ANSI C
 PROMELA
 Finitestate transition systems
 LTL
 Explicit

Truth
 Aachen University of Technology
 Haskell/Java
 CCS
 Finitestate transition systems
 Modal mucalculus
 Explicit, tableaubased

UPPAAL
 Uppsala and Aalborg University
 C++
 Timed automata
 ?
 Safety/liveness properties
 ?
