The SMV (Symbolic Model Verifier) system is a tool for 
checking finite state systems against specifications 
in the temporal logic CTL (Computational Tree Logic). 

One specifies the finite state system (finite automaton,
Mealy machine, full adder circuit, ..) as a Kripke 
structure in the SMV language and provides specifications 
in CTL. The model checking algorithm allows to determine 
if the Kripke structure fulfills the specifications.

WWW: http://www.cs.cmu.edu/~modelcheck/smv.html