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 BDDbased
symbolic model checking for CTL and LTL, and SATbased 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 Zerosuppressed 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 QuantifierFree Linear Arithmetic Logic and QuantifierFree 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.
