My interests span three areas: Programming Systems, Hardware, and Theory. I use techniques from theoretical computer science to solve problems in programming systems and hardware design that are of practical interest. During the last 30+ years my research has focused on Model Checking and the formal verification of hardware and software correctness.

It is well known that logical errors in finite state concurrent systems, such as sequential circuits and communication protocols, are an important problem for computer scientists. They can delay getting a new product on the market or cause the failure of some critical device that is already in use. The most widely used verification method is based on extensive simulation and can easily miss significant errors when the number possible states of the system are very large. Although there has been considerable research on the use of theorem provers, term rewriting systems, and proof checkers for verification, these techniques are time consuming and often require a great deal of manual intervention. In joint research with my student Allen Emerson, we developed an alternative approach called Model Checking. In this approach specifications are expressed in a propositional temporal logic, and an efficient search procedure is used to determine whether or not the specifications are satisfied.

Since the original Model Checking algorithm was published, the size of the systems that can be verified has increased dramatically. By developing special programming languages for describing transition systems, it became possible to check examples with several thousand states. This was sufficient to find subtle errors in a number of nontrivial, although relatively small, circuit and protocol designs. In joint research with Burch, Dill and McMillan, we showed how the transition relation of a finite state system could be represented symbolically. Use of ordered binary decision diagrams (OBDDs) led to a major increase in the size of the examples we could handle. Representing transition relations implicitly using OBDDs made it possible to verify examples that would have required 10²⁰ states with the original version of the Model Checking algorithm. Refinements of the OBDD-based techniques have pushed the state count up over 10¹⁰⁰ states. By combining Model Checking with abstraction, we have been able to check even larger examples. In one case we were able to verify a pipelined ALU design with 64 registers, each 64 bits wide, and more than 10¹³⁰⁰ reachable states.

The size and complexity of the systems we can verify by Model Checking techniques continues to grow. In joint research with Biere, Cimatti, and Zhu, we developed a technique called Bounded Model Checking. This was one of the first applications to demonstrate the power of fast propositional SAT solvers. In joint research with Grumberg, Jha, Lu, Veith, we developed a powerful new abstraction technique called CounterExample Guided Abstraction Refinement (CEGAR). Currently Sicun Gao, Soonho Kong, and I are investigating Model Checking techniques for hybrid systems with nonlinear dynamics. We believe that this research will be particularly important for verifying embedded systems in automotive and aerospace applications where the behavior of the environment is governed by a differential equation.

Model Checking is routinely used for verification of computer hardware and protocols in industry. It is beginning to be used for computer software as well, although this problem is much harder and will require new data structures and abstraction techniques to deal with the enormous state spaces involved. Model Checking can also be combined with automated theorem proving and benefit from the power of this approach to verification. I am quite confident that Model Checking will continue to scale to ever larger systems in which absolute correctness is essential.