Symbolic model checking is an automatic verification paradigm for checking temporal properties (e.g., safety, liveness, fairness) of finite state systems. It has been successfully applied to a variety of applications, ranging from hardware designs to software protocols. The technology enabling these successes is the use of Binary Decision Diagrams (BDDs) to perform symbolic computation.

BDD computations are both time and space intensive and their computational characteristics are not well understood. In this talk, I will address this issue at two levels. At the low level, I will present an evaluation methodology for systematically studying BDD computation. Application of this methodology to model checking computations led to better understanding of the computation and significant performance improvements. At the high level, I will describe a new algorithm to reduce the state space for a special class of constraint-rich models. Together, these optimizations resulted in a powerful model checker which enabled verification of the fault diagnosis model of the NASA Deep Space One spacecraft.