Abstract: A model checking-based program analysis method was proposed. The main steps include translating C/C++ source code into Kripke structure that is equivalent to control flow graph, describing properties of source code in CTL formula and verifying the program using model checker NuSMV. Based on this idea, a tool which is used to automatically translate C/C++ source code into NuSMV input was designed and implemented. The experiments show that this approach is able to analyze the program effectively.

Key words: Model checking, Program analysis,Automatic NuSMV input tool