Ken McMillan's Home Page


Ken McMillan
Cadence Berkeley Labs
2150 Shattuck Ave., 10th floor
Berkeley, CA  94704
mcmillan@cadence.com

I'm a researcher at Cadence Berkeley Labs in Berkeley, CA.  My main area of research is formal verfication of computer hardware and software.   Currently, I'm working primarily on model checking methods based on SAT and Craig interpolants. On this site, you'll find an interpolating decision procedure called FOCI, that has various applications in infinite-state model checking.

I've also worked on a system called "SMV", which uses a technique called "symbolic model checking" to formally verify that hardware designs satisfy their specifications.   SMV also implements "compositional methods" that allow you to verify large, complex systems by reducing the verification problem to small problems that can be solved automatically by model checking.  SMV provides a variety of techniques for this purpose, including refinement verification, temporal case splitting, symmetry reductions, data type reductions, and uninterpreted functions.  There are a few technical reports available on this site describing these methods.  It is probably best to start with the overview. However, the best way to learn about these methods is probably to download the SMV system and try it out. The software download includes an online tutorial that introduces the various features of SMV by example.

If you are visiting Cadence Berkeley Labs, and need directions, click here.