Computer-Aided Verification Tools

Original link:
The following tools were demonstrated at CAV 96 or CAV 97.
CADP (Caesar-Aldebaran Distribution Package):
a protocol validation and verification toolset
The Concurrency Factory:
a graphical environment for specification, simulation, verification, and implementation of concurrent systems
Fc2Tools & Auto/Graph:
a symbolic/explicit verification toolset for concurrent processes
a symbolic model checker for embedded systems
Invariant Checker:
automated deductive verification of reactive systems
formal verification of real-time systems based on timed automata and temporal logic
MDG (Multiway Decision Graphs):
abstract state enumeration for RTL functional verification
tool integration and engineering environment for the organization and synthesis of large-grain software systems
a decision procedure for monadic second-order logic over finite strings
a model checker
finite-state verification of high-level concurrent systems, such as protocols, synchronization algorithms, and memory-model specifications
a tool for visual specification and verification of distributed real-time systems
Partial-order Package:
an extension of SPIN
PEP (Programming Environment based on Petri nets):
modeling, simulation, analysis, and verification of parallel systems
PNN (Product Net Machine) & SH-Verification Tool:
a specification and verification tool for cooperating systems
a Pr/T-net reachability analysis tool that supports verification with partial-order reductions
a verification system
RTGIL (Real-Time Graphical Interval Logic) Tools:
graphical editor, satisfiability checker, counterexample generator, database and proof manager for concurrent real-time systems
symmetry-based model checker for verification under fairness assumptions
an efficient LTL model checker for distributed software designs
STeP (The Stanford Temporal Prover):
verification of reactive and real-time systems
a system for checking the termination of queries to logic programs
validation and verification tools for real-time systems
automatic detection of coordination problems between concurrent processes executing arbitrary (e.g., C or C++) code
a system for verification and synthesis

More verification tools can be found at the Oxford Formal Methods home page.
Last updated in April, 1997, by