Since the dawn of computing, engineers have checked for logic errors in computer circuitry or software programs by running simulations to test performance and by manually checking each line of computer code. But as computer chips grew to include hundreds of thousands or millions of transistors, and as software and computer systems similarly grew in complexity, these hit-or-miss “informal verification” methods became inadequate to the task. Errors often went undetected until after a product was released, when correcting even minor errors is expensive.

Model Checking, by contrast, is a type of “formal verification” that analyzes the logic underlying a design, much as a mathematician uses a proof to determine that a theorem is correct. Far from hit or miss, Model Checking considers every possible state of a hardware or software design and determines if it is consistent with the designer’s specifications.

“The influence of Model Checking on both theory and practice has been tremendous, but the full impact is still ahead of us,” said Peter Lee, professor and head of Carnegie Mellon’s Computer Science Department. “Ideas based on Model Checking are getting us closer to new software development methods that may, for the first time, give us programs that actually work as specified.”

Clarke and Emerson originated the idea of Model Checking at Harvard in 1981. They developed a theoretical technique for determining whether an abstract model of a hardware or software design satisfies a formal specification, given as a formula in Temporal Logic, a notation for describing possible sequences of events. Moreover, when the system fails the specification, it could identify a counterexample to show the source of the problem.

When Clarke joined Carnegie Mellon in 1982, he implemented the first Model Checker. It could analyze all the possible states of a given circuit, but was limited to relatively small designs — much smaller than the systems being built by computer manufacturers.

In 1987, Clarke’s graduate student, Kenneth McMillan, realized that he could implement Model Checking by a series of operations on binary decision diagrams (BDDs), a method of representing symbolic information that had recently been developed by another Carnegie Mellon computer science professor, Randal E. Bryant. This new system, called Symbolic Model Checking, was able to analyze billions of billions of states, making it relevant to commercial computer design problems and leading to its widespread adoption by the industry. For this invention, Bryant, Clarke, Emerson and McMillan won the 1998 Paris Kanellakis Award for Theory and Practice from the ACM. In 1999, they also received the Allen Newell Award for Research Excellence from Carnegie Mellon.