Ken McMillan's Home Page
kenmcmil at my employer dot com
This page is under construction. Meanwhile, the links below are old but possibly useful.
Cadence SMV and other downloads from Cadence Berkeley Labs
SMV case studies.
(CAV'01 and CHARME'01).
Benchmarks for SAT solvers based on bounded model checking
Sample implementation of interpolation procedure from TACAS04
: symbolic model checking
: interpolating prover
Benchmarks used in publications
Technical reports available on-line
Slides from talks
Tutorial on formal verification
Tutorial on SMV
The SMV system (in postscript)
Symbolic Model Checking