近年来,软件应用在工业、农业、军事、科研等领域有了更加广泛的应用。随着应用的更广泛,代码规模的增大、软件系统的复杂度提高、程序中可能出现的各种错误漏洞也越来越多。因此,提高软件系统的安全性与可靠性,保证程序代码的正确性与规范性变的尤为重要。随着SMT求解器的迅速发展,模型检测已经被广泛的使用在代码级别的软件系统的验证,并且一些软件模型检测工具不断发展和不断成熟使得它们可以支持大规模软件系统的验证。模型检测方法的一个显著优点是当期望的性质不满足时能够提供程序违背该性质的反例路径。C语言是程序开发时经常使用的编程语言之一。由于C程序具有灵活的内存管理机制,在C程序中经常会涉及到很多内存的动态分配与使用。但是如果动态分配的内存在使用完后没有及时释放掉会导致程序发生内存泄漏,甚至直接导致程序奔溃。本文研究如何基于软件模型检测工具提供的反例路径去修复C程序中存在的内存泄漏。首先,利用模型检测工具TPChecker自动检测C程序中存在的内存泄漏,并生成泄漏的内存空间对应的所有反例路径。TPChecker是在CEGAR算法改进的基础上实现的。其次,得到所有的反例路径之后,从这些反例路径上提取出与内存分配和使用相关的信息,并把这些信息映射到C程序的控制流自动机上。最后,根据能够正确修复内存泄漏并保证程序正确性的规则对C程序进行安全的修复并得到修复之后的C程序文件。基于本文提出的方法,将检测内存泄漏的部分和修复内存泄漏的部分进行结合,实现了工具CEGFixer用于修复C程序中的内存泄漏。本文将CEGFixer与前沿的内存泄漏修复工具Leakfix进行实验比较。实验结果表明CEGFixer在修复C程序中的内存泄漏方法有着很不错的效果,不仅提高了修复C程序中内存泄漏的比率,而且能够修复的内存泄漏类型比Leakfix多。