Satisfiability-based abstraction refinement in symbolic model checking

Model checking has been widely used in hardware and software designs. Currently, due to the state explosion problem, the main bottleneck in model checking is the capacity of handling large designs. How to extend the capacity of model checkers is an intriguing topic.; Among techniques to reduce the state explosion problem, abstraction refinement is an efficient one. In this thesis, a couple of satisfiability-based, fully automatic abstraction refinement approaches are proposed, which greatly enhance the ability of model checker to deal with large scale models.; First, in contrast to current BDD-based or BDD-SAT hybrid abstraction refinement engine, a purely SAT base abstraction refinement framework, named PureSAT, is proposed. This is also the first time an abstraction refinement totally based on SAT solvers is proposed.; Second, due to the fact that normal SAT solvers are not suitable for the application of abstraction refinement, an Abstraction Refinement Oriented SAT solver (AROSAT) is designed which generates more compact refinements than normal SAT solvers by bring in only necessary memory elements into unsatisfiability proofs. Although AROSAT takes longer time to finish, applying it in abstraction refinement would pay off by saving big time in refinement computation.; Third, because SAT solvers internally behave like abstraction refinement engines, an interesting question is whether we can still profitably combine abstraction refinement with SAT based model checking techniques. To investigate this question, we combined abstraction refinement and interpolation algorithm and also developed various techniques which significantly lowered the cost for computing refinements. Experiments show that we can still profitably combine abstraction refinement with efficient SAT-based algorithms.; Fourth, to answer the question how PureSAT does compared with BDD-SAT hybrid abstraction refinement frameworks, we compared PureSAT with Grab, which has a similar abstraction refinement framework as PureSAT, but is based on a BDD-SAT hybrid engine. The results show that PureSAT is more robust in general cases.; Finally, we gave full evaluations to the PureSAT algorithm.; Analytical and experimental studies show that by applying techniques proposed in this thesis, the capacity of dealing with large scale designs of model checkers can be greatly enhanced.