Research on Model Checking Based Source Code Analysis
Rong Li · Microelectronics & Computer · 2009
A model checking-based source code analysis method is proposed and implemented in this paper. 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 source code using model checker NuSMV. The experiments show that this approach is able to achieve the goal of source code analysis.