HTTP/2 200 last-modified: Mon, 09 Dec 2019 05:30:04 GMT accept-ranges: bytes content-length: 2412 content-type: text/html date: Wed, 14 Jan 2026 23:22:11 GMT server: Apache 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