Abstract: Model checking on software reliability is always considered meaningful. This paper studied theory and methodology on source code verification, utilizing predicate abstraction and counterexample-guided abstraction refinement. Detailed verification framewor

Key words: Software model checking, Source verification, Predicate abstraction,Abstraction refinement