Chao Wang (Ph.D., University of Colorado at Boulder, 2004)

Model checking is a formal method for proving that a finite state transition system satisfies a user-defined specification. The primary obstacle to its widespread application is the capacity problem: the state-of-the-art model checker cannot directly handle most industrial-scale designs. Abstraction refinement, an iterative process of synthesizing a simplified model to help verifying the original model, is a promising solution to the capacity problem. In this thesis, several fully automatatic abstraction refinement techniques are proposed to efficiently reach or come near to the simplest abstraction.

First, a fine-grain abstraction approach is proposed to keep the abstraction granularity small. With the advantage of including only the relevant information, fine-grain abstraction is proven indispensable in verifying systems with complex combinational logics. Second, a refinement algorithm is proposed to identify the refinement information based on the systematic analysis of all the shortest counter-examples. Compared to single counter-example guided algorithms, this algorithm often produces a smaller abstract model that can prove or refute the same property. Third, a compositional SCC analysis algorithm is proposed to quickly identify unimportant parts of the state space and prune them away before verification is applied to the next abstraction level. With a speed-up of up to two orders of magintude over standard model checking algorithms, it demonstrates the importance of reusing information learned from previous abstraction levels. Finally, BDD based symbolic image computation and Boolean satisfiability are studied. Two new algorithms are proposed to improve their computational efficiency by applying the abstraction and the successive refinements inside the two basic decision procedures. Analytical and experimental studies demonstrate that the fully automatic abstraction refinement techniques proposed in this thesis are the key to applying model checking to large systems.