ACM Paris Kanellakis Theory and Practice Award
Cadence Berkeley Labs United States – 1998

Symbolic Model Checking

Randal E. Bryant, Edmund M. Clarke, E. Allen Emerson, Kenneth L. McMillan

For their invention of symbolic model checking, a method of formally checking system designs, which is widely used in the computer hardware industry and is beginning to show significant promise also in software verification and other areas.

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.