Abstract: Buffer overflow (BO) vulnerability in C programs is one of the most crucial threats to the security of a system. Using tools to detect and eliminate this kind of vulnerability in programs will give the system sufficient ability to maintain security environment. For the scarcity of accuracy in detecting BO vulnerabilities, current bug-hunting tools can not precisely detect BO vulnerabilities. A new method was proposed, which uses model checking, to precisely detect potential BO in C programs. This method converts detecting BO vulnerabilities to verifying the reachability of certain position in programs and uses model checking tool to do the verification job. Using this method, a prototype system has been developed and been tested with some benchmarks. The early results show that this method can precisely detect BO vulnerabilities in C programs.