Abstract: How to assure the correctness and reliability of software systems is one of the main problems in software development. Being an important automatic verification technique, Model checking is more and more successful in software analysis and verification. T

Key words: Model checking, Software model checking,Predicate abstraction,Counterexample-driven refinement