Symbolic Model Verifier is a model checker for finite-state systems, using the specification language CTL (Computation Tree Logic), a propositional branching- time temporal logic. SMV is from CMU.
SMV Manual (local copy)
Download SMV version
2.54 for UNIX (gzip file)
Download SMV version 2.5 for
Windows NT (winzip file)