Source-oriented Software Model Checking and its Implementation
面向源代码的软件模型检测及其实现

Model checking on software reliability is always considered meaningful.This paper studied theory and metho-dology on source code verification,utilizing predicate abstraction and counterexample-guided abstraction refinement.Detailed verification framework and its implementation of the self-designed Jchecker,a source-oriented software model checker,were also introduced.