Experience

Sign in to view more

Education

Sign in to view more

Bio

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.

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.