2fadfa2cfb
e-mail addresses from the pkg-descr file that could reasonably be mistaken for maintainer contact information in order to avoid confusion on the part of users looking for support. As a pleasant side effect this also avoids confusion and/or frustration for people who are no longer maintaining those ports.
11 lines
494 B
Text
11 lines
494 B
Text
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
|