Randal E Bryant
ACM Fellows
USA - 2000
citation
Randal Bryant is best known for Ordered Binary Decision Diagrams, a canonical form for boolean functions. Although originally developed for applications in CAD, this data structure has found many applications in areas such as hardware and software verification, automated theorem proving, and AI planning.
ACM Paris Kanellakis Theory and Practice Award
USA - 1998
citation
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.