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 compositinonality and abstraction 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.
Formal verification, model checking, program analysis, decision procedures and automated theorm provers, abstraction refinement, compositional methods, parameterized systems, Craig interpolation.
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.