[I2 logo] [RWTH logo] MOVES: Software Modeling and Verification
(Informatik 2)
Computer Science / RWTH / I2 / Research / AG / MCS / Tools

Tools for the Specification and Verification of Concurrent Systems


Tool Developer Implementation language System description language Semantic model Logic Model checking algorithm
Circal University of South Australia ? XCircal Finite-state transition systems ? (1) Explicit
(2) OBDD-based
Concurrency Factory SUNY at Stony Brook, NC State University C++ VPL (compiled into Facile) Finite-state transition systems Linear-time alternation-free modal mu-calculus Explicit
Edinburgh Concurrency Workbench University of Edinburgh Standard ML CCS Finite-state transition systems Modal mu-calculus Explicit
FC2Tools INRIA, Ecole des Mines ? Process algebra Finite-state transition systems ? ?
FDR2 Formal Systems Design and Development Inc. ? CSP Finite-state transition systems ? Symbolic, on-the-fly
HyTech University of Berkeley C++ Linear hybrid automata ? ICTL Symbolic, region-based
JACK Tool Set University of Pisa Several Transition systems ? ACTL ?
Kronos VERIMAG ? Timed automata ? TCTL Symbolic, constraint-based
Mobility Workbench Universities of Edinburgh and Uppsala Standard ML Pi-calculus Transition systems (only equivalence checking) Explicit, on-the-fly
Model-Checking 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) Finite-state transition systems Modal mu-calculus 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 Carnegie-Mellon University ? Automaton Finite-state transition systems CTL Symbolic, OBDD-based
SPIN Bell Laboratories ANSI C PROMELA Finite-state transition systems LTL Explicit
Truth Aachen University of Technology Haskell/Java CCS Finite-state transition systems Modal mu-calculus Explicit, tableau-based
UPPAAL Uppsala and Aalborg University C++ Timed automata ? Safety/liveness properties ?

Further Collections

Valid HTML 4.01 Strict! Valid CSS!