« Back to Page 1

Clarke clearly remembers his awestruck but frustrating encounters with the first computer to appear on the University of Virginia campus during his undergraduate days there. The crude machine was enclosed behind glass, and users had to line up to submit punched program cards to the computer operator. The job would generate a printout containing final results or, all too often, an abort notice with an attached error log. Sometimes it would take a full day just to get back an output that showed a mistake in the program.

"Maybe that led to my interest in finding errors and bugs," muses Clarke, tugging on the salt-and-pepper wisps of his neatly trimmed beard.

Clarke earned a master's degree in mathematics from Duke University in 1968 and then went on to complete his PhD in computer science at Cornell University, writing his dissertation on highly theoretical aspects of how to prove the correctness of computer programs.

"I enjoyed writing the thesis and doing the research, but I was a little disappointed that the results had no practical application whatsoever," he says.

He returned to Duke for two years and then moved to Harvard, where he and Emerson developed the theoretical underpinnings of Model Checking.

Model Checking is a type of formal verification that examines the logic underlying a design, much like a mathematician uses a proof to figure out whether a theorem is correct. It works like this: First, the design of the chip or software being analyzed is converted into an abstract model. The specifications of the model are next expressed in a special type of notation called temporal logic, a language which describes how the system will behave over time. Then, true to its name, the Model Checker indeed checks every last possible state of the model and determines whether it is consistent with the specifications.

After arriving at Carnegie Mellon, Clarke decides to put this "practical application" to the test. He steals away to his basement office for a few hours every morning to write the computer code for the first Model Checker. Then he begins testing his algorithm with small example problems, trying to see whether it can automatically catch mistakes he knows they contain. Time and again, he gets answers that he thinks are incorrect, suspecting there is a bug in his model checking code. By Christmas, however, Clarke begins to realize the bugs aren't in the Model Checker; they are errors in the examples themselves that he didn't know existed.

"That's when I knew this was going to be a really important idea," he recalls.

Unlike simulation and testing, Model Checking has the benefits of being fully automatic, fast, and exhaustive in its search for errors. Moreover, when a design fails to satisfy a desired specification, the method always identifies a counterexample that reveals the source of the problem and often provides important clues for how to fix it.

But there is one serious drawback in the Model Checker.

As the complexity of a system increases, the number of possible states that must be analyzed multiplies exponentially, overwhelming the Model Checker. This conundrum--called the state explosion problem--seems to limit the applicability of the technique to small designs mainly of interest to academia, not industry.

"This is the problem that I've been struggling with for the past 26 years," says Clarke, now the FORE Systems University Professor of Computer Science and professor of Electrical and Computer Engineering at Carnegie Mellon.

In the fall of 1987, Clarke discusses the state explosion problem during a lecture in which computer science faculty introduce their research to incoming PhD candidates. Among those listening is first-year graduate student Kenneth McMillan.

McMillan also hears a presentation by Randal Bryant, now University Professor and dean of Carnegie Mellon's School of Computer Science, whose research focuses on formal verification of computer hardware. Bryant had invented a method of encoding information symbolically called binary decision diagrams.

Not long after the two lectures, McMillan lies out on The Cut to catch some sunshine, his mind spinning in full gear as Frisbees fly overhead.

"I started wondering if you could use [Bryant's] diagrams to model a system with a lot of components as a way to avoid the state explosion problem," says McMillan, who is now a researcher studying formal verification of computer hardware at Cadence Berkeley Labs in California.

(Continued …)

1 2 3