Model Checking @CMU
Several packages are available below, or via ftp. There are also instructions on how to use ftp . We are glad to provide this code, and encourage suggestions and comments. However, we do not give any guarantees. Please see the license agreement for details.
NFLSAT- Non-clausal SAT solver based on DPLL and Negation Normal Form (NNF)[new!]
SatMate - Satisfiability Checking of using General Matings
VCEGAR - Verilog CounterExample Guided Abstraction Refinement [new!]
CBMC - C Bounded Model Checker[new!]
MAGIC - Modular Analysis of proGrams in C [new!]
smv2vcd - A Perl script to convert an SMV/NuSMV counterexample to industry standard Value Change Dump (VCD) format.
SyMP - Symbolic Model Prover, a tool for combining Model Checking and Theorem Proving
Bounded Model Checker (BMC) is now available!
SMV - a symbolic model checker for CTL [latest revision 2.5].
A BDD library with extensions for sequential verification.
CSML and MCB - a language for compositional description of finite state machines and a (non-symbolic) model checker for CTL.
CV - A Model Checker for VHDL. This page is going to be reorganized and updated soon, watch for new stuff.
Word-level SMV can be used to verify arithmetic circuits efficiently.
Verus - a new model checker with a nicer input language, real time and a lot of other features.
Please send any comments and suggestions to Nishant Sinha - (nishants) at cs dot cmu dot edu.