Abstraction refinement for large scale model checking

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. granularity small. With the advantage of including only the relevant information, 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 the same property. Third, a compositional SCC analysis algorithm is proposed to quickly identify unimportant parts of the state space and prune them away of up to two orders of magnitude over standard model checking algorithms, it demonstrates the importance of reusing information learned from previous satisfiability are studied. Two new algorithms are proposed to improve their inside the two basic decision procedures. Analytical and experimental studies in this thesis are the key to applying model checking to large systems.