Kenneth L. McMillan

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.