In problem of software logic errors, nowadays it emerges more and more. The paper presents the research for model checking methods of C language, that it is the most popular and general programming languages. The model checking based on Verds tools, using C language subset into Verds model algorithm, combined with the Verds tools and MAGIC tools. Introducing the counterexample guided abstraction refinement (CEGAR) method to solve the problem of state explosion.