VIS (Verification Interacting with Synthesis)

VIS is a system for formal verification, synthesis, and simulation of finite state systems. The formal verification part includes both BDD-based symbolic model checking for CTL and LTL, and SAT-based bounded model checking. 

CUDD (CU Decision Diagram Package)

CUDD is a package for the manipulation of Binary Decision Diagrams (BDDs), Algebraic Decision Diagrams (ADDs) and Zero-suppressed Binary Decision Diagrams (ZDDs). You can also download DDcal, a BDD calculator based on CUDD, PerlDD, an extension to Perl based on CUDD, and a collection of BDD variable orders. 

Wring

Wring is a program to translate Linear Time Logic (LTL) formulae into generalized Buechi automata. Wring is written in Perl. 

SATEEN

SatEEn is an SMT solver that deals with Quantifier-Free Linear Arithmetic Logic and Quantifier-Free Difference Logic. 

N_ABLE  (Action Based Learning for switching and automata theory)

N_ABLE consists of many interactive learning games for students interested in logic synthesis and verification. It is written in Java applets.