Ken McMillan's Home Page

Ken McMillan
Microsoft Research
kenmcmil at my employer dot com

This page is under construction. Meanwhile, the links below are old but possibly useful.

• Download
  • 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
• Publications
• Tools
• Cadence SMV: symbolic model checking
• FOCI: interpolating prover
• Benchmarks used in publications
• Technical reports available on-line
• Slides from talks
• Tutorials
  • Tutorial on formal verification
  • Tutorial on SMV
• Software documentation
  • The SMV system (in postscript)
• Thesis: Symbolic Model Checking