Portrait of Kenneth McMillan

Kenneth McMillan

Principal Researcher

About

My primary research area is formal methods. I have worked on topics such as symbolic model checking, Petri net unfoldings, automated abstraction, compositional methods, Craig interpolation, deductive verification and specification-based testing.

I started out as an electrical engineer, designing chips and biomedical instruments. My undergraduate degree is in EE, from the University of Illinois, and I also have an MSEE from Stanford. This experience got me interested in the process of designing complex systems, and in particular, how we determine that complex system designs are correct. I switched to computer science, doing my Ph.D. with Ed Clarke at CMU, graduating in 1992. My thesis was on a technique called Symbolic Model Checking (SMV) that could be used to verify logical properties of finite-state systems by efficiently exploring very large state spaces. I developed a model checker called SMV that implemented these techniques, as well as other techniques for combatting the so-called state explosion problem.

I went on to do research at Bell Labs, Cadence Berkeley Labs, and now (as of 2010) Microsoft Research. At Cadence, I further developed SMV, incorporating methods of compositionality and abstraction to break large verification problems down into small ones in a tool called Cadence SMV. Later, I became interested in the question of relevance. That is, if you want to prove a logical property of a complex object like an computer program or a hardware design, how do you decide what information about that system is relevant to that property? This led to a technique called Craig interpolation that allows us to use logical proof as a basis for relevance, and can be used as the foundation of formal verification tools for hardware and software. Most recently, I have been exploring issues of usability in formal methods, especially in the area of distributed systems. For example, how do we make best use of powerful proof automation tools to productively design and prove systems? How can we obtain useful formal descriptions of complex protocols? This work is embodied in a tool called Ivy.

On my personal home page, you can find information about my current research, including projects, papers, talks, tools and so on. If you are looking for a paper of mine, a full list of publications (with PDF files for most) can be found on my publications page.

Research interests

Formal verification, model checking, program analysis, decision procedures and automated theorm provers, abstraction refinement, compositional methods, parameterized systems, Craig interpolation.

Current projects

My current projects include an interpolating version of the highly efficient SMT solver Z3, as well as tools for abstraction refinement, invariant generation and model checking based on interpolation. I’m also interested in the use of symbolic algorithms in other fields and am currently working on an application of constraint solving in education and human-computer interaction in the form of an elementary geometry tutor.