Model Checking @CMU










Model Checking Code Available

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.





CMU-SCS Model Checking home page

Please send any comments and suggestions to  Nishant Sinha - (nishants) at cs dot cmu dot edu.