CProver is a tool for the formal verification of ANSI-C programs and
hardware designs given in a description language such as Verilog or VHDL.
CheckMate is a verification tool for hybrid dynamic systems, that is,
dynamic systems with both discrete and continuous state variables. Hybrid
systems often arise in computer-control systems where the discrete dynamics
corresponds to the control logic and the continuous dynamics corresponds to
the physical system being controlled.
- Model Checkers
Model Checkers such as SMV have been applied successfully in many different
domains, e.g., hardware and protocol verification.
Ymer is a tool for verifying probabilistic transient properties of
continuous-time Markov chains (CTMCs) and generalized semi-Markov processes
(GSMPs). Properties are expressed using the Continuous Stochastic Logic
SF2SMV uses Model Checking to formally verify Stateflow diagrams.
UCLID is a tool for modeling and verifying systems at a term
level, with both Boolean and integer data types, uinterpreted functions,
and restricted forms of integer arithmetic. It consists of a modeling
language, a symbolic simulator, and a set of decision procedures. It can
be used in three modes: as a bounded property checker, to verify pipelined
processors, and to prove inductive invariants.