Formal verification, model checking, program analysis, decision procedures and automated theorm provers, abstraction refinement, compositional methods, parameterized systems, Craig interpolation.
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 comnplex 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 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 compositinonality and abtrsction to break large verification problems down into small ones in a tool called Cadence SMV. More recently, I've been mainly 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 lead 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.
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.
For more information on my work before joining Microsoft Research, including downloads of Cadence SMV, FOCI, and other materials, see my personal home page.
- Shuvendu Lahiri, Ken McMillan, Rahul Sharma, and Chris Hawblitzel, Differential Assertion Checking, in Foundations of Software Engineering (FSE'13), ACM, August 2013
- Nikolaj Bjorner, Kenneth L. McMillan, and Andrey Rybalchenko, On Solving Universally Quantified Horn Clauses, in Static Analysis Symposium, Springer, 20 June 2013
- Boyang Li, Isil Dillig, Thomas Dillig, Kenneth L. McMillan, and Mooly Sagiv, Synthesis of Circular Compositional Program Proofs via Abduction, in 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Springer, 16 March 2013
- Shuvendu K. Lahiri, Kenneth L. McMillan, Rahul Sharma, and Chris Hawblitzel, Differential Assertion Checking, no. MSR-TR-2013-34, March 2013
- Kenneth McMillan and Andrey Rybalchenko, Computing Relational Fixed Points using Interpolation, no. MSR-TR-2013-6, 17 January 2013
- Nikolaj Bjorner, Kenneth L. McMillan, and Andrey Rybalchenko, Program Verification as Satisfiability Modulo Theories, in 10th International Workshop on Satisfiability Modulo Theories, 30 June 2012
- Kenneth L. McMillan, Interpolants from Z3 proofs, in Formal Methods in Computer-Aided Design, 30 October 2011