随着人类对于软件的使用越来越广泛普遍，研究越来越深入，对其精确度的要求也越来越高。程序的语法错误可以在相应的平台上完成检测，但是并没有完成程序逻辑检测。针对软件逻辑错误检测这个问题，提出了对最流行普遍使用的编程语言——C语言子集的模型检测方法的研究，提出在模型检测工具下C语言子集的性质验证。针对C语言模型检测中，存在的状态爆炸问题借鉴使用合适的解决方法，减少模型检测中冗余的状态。希望解决C语言子集程序逻辑验证问题，实现C语言子集程序自动化验证，完成对C程序的性质验证。　　 Verds作为模型检测工具，具有一定优势，本文提出在此工具中进行C语言子集的模型检测，减少了建立模型的过程;其次对于简单的C语言程序，给出将C语言子集转化到Verds模型的算法，实现C语言子集程序在Verds工具上的自动验证;然后针对大程序存在的状态空间爆炸问题，引入反例引导的抽象精化(CEGAR)方法处理模型检测中存在的状态空间问题。　　 总之，本文主要创新在以下几个方面:　　 (1)提出在Verds模型检测工具上对C语言的模型检测，在Verds模型下实现对C语言子集程序的性质验证。　　 (2)实现C语言子集程序到Verds模型的转化，完成将常用的C语言子集程序自动转化成Verds模型的工作。　　 (3)引入CEGAR方法处理C语言子集大程序的模型检测中存在的状态爆炸问题，提高模型检测效率。