Abstract:

To overcome the state space explosion problem in model checking, a CPAChecker based dynamic program verification approach is proposed. The proposed approach first verifies the program statically by unwinding the control flow chart. In the process, dynamic execution is applied to accelerate the verification on the basis of the determinism of branch statements. Specifically, abstract verification effectively reduces the size of the system models, while dynamic detection not only effectively reduces false positives, but also guides the construction of more accurate system models. As a result, the proposed approach makes counterexample-guided abstraction refinement more efficient and accurate in practice.

Key words: model checking, abstract refinement, dynamic execution, program verification, state space explosion