Edmund M. Clarke

Edmund Clarke

University Professor, Emeritus

Office: 9231 Gates & Hillman Centers

Email: ec10@andrew.cmu.edu

Phone: (412) 268-2628

My interests span three areas: Programming Systems, Hardware, and Theory. I use the techniques and insights of theoretical computer science to solve problems in programming systems and hardware design that are of practical interest. I have a number of active research projects in these areas that I would be happy to discuss with students. Below are short descriptions of two research projects that I think are particularly exciting.

Hardware and Software Verification. Logical errors in finite state concurrent systems like 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 is 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. My group has developed an alternative approach called temporal logic model checking in which specifications are expressed in a propositional temporal logic and an efficient search procedure is used to determine whether or not the specifications are satisfied.

In the twenty-five years that have passed since the original algorithm was published, the size of the systems that can be verified by this means 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 protocols designs. Use of boolean decision diagrams (BDDs) led to a major increase in the size of the examples we could handle by this technique. Representing transition relations implicitly using BDDs made it possible to verify examples that would have required 1020 states with the original version algorithm. Refinements of the BDD-based techniques have pushed the state count up over 10100 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 101300 reachable states.

Analytica --- A Theorem Prover for Mathematica.  Analytica is an automatic theorem prover for theorems in elementary analysis. The prover runs in the Mathematica environment and is written in Mathematica language. The goal of the project is to use a powerful symbolic computation system to prove theorems that are beyond the scope of previous automatic theorem provers. The theorem prover is also able to guarantee the correctness of certain steps that are made by the symbolic computation system and therefore prevent common errors like division by a expression that could be zero.

Since we wanted to generate proofs that were as similar as possible to proofs constructed by humans, we use a variant of natural deduction to generate proofs. We have demonstrated the power of our theorem prover on several non-trivial examples including the basic properties of the stereographic projection and a series of three lemmas that lead to a proof of Weierstrass's example of a continuous nowhere differentiable function. Each of the lemmas in the latter example is proved completely automatically. In a related project that uses similar techniques, we have managed to prove all of the theorems and examples in Chapter 2 of Ramanujan's Collected Works completely automatically. We believe these examples provide convincing justification for combining powerful symbolic computation techniques with theorem provers.