Edmund Clarke

In 1981, Edmund M. Clarke and E. Allen Emerson, working in the USA, and Joseph Sifakis working independently in France, authored seminal papers that founded what has become the highly successful field of Model Checking. This verification technology provides an algorithmic means of determining whether an abstract model--representing, for example, a hardware or software design--satisfies a formal specification expressed as a temporal logic formula. Moreover, if the property does not hold, the method identifies a counterexample execution that shows the source of the problem. The progression of Model Checking to the point where it can be successfully used for complex systems has required the development of sophisticated means of coping with what is known as the state explosion problem. Great strides have been made on this problem over the past 27 years by what is now a very large international research community. As a result many major hardware and software companies are now using Model Checking in practice. Examples of its use include the verification of VLSI circuits, communication protocols, software device drivers, real-time embedded systems, and security algorithms.

The work of Drs. Clarke, Emerson, and Sifakis continues to be central to the success of this research area. Their work over the years has led to the creation of new logics for specification, new verification algorithms, and surprising theoretical results. Model Checking tools, created by both academic and industrial teams, have resulted in an entirely novel approach to verification and test case generation. This approach, for example, often enables engineers in the electronics industry to design complex systems with considerable assurance regarding the correctness of their initial designs.

Model checking was invented in 1981 by Clarke and Emerson. This technique made it possible to algorithmically verify logical properties, expressed in a notation called temporal logic, of finite-state systems. Clarke and Emerson were able to use model checking to find some very subtle design errors in published hardware designs. The size of the state space was seriously limited, however, by the amount of available computer memory. In 1985, Bryant developed a new representation of Boolean functions, called OBDDs (Ordered Binary Decision Diagrams). Bryant's crucial contribution was to show that by fixing the order of testing of Boolean variables in binary decision diagrams, these diagrams become very tractable computationally. McMillan then realized that OBDDs can symbolically represent sets of states in state-transition systems. In 1987, he developed a software tool called SMV (Symbolic Model Verifier) with which systems with over 10^20 states could be verified, and symbolic model checking was born.