随着计算机硬件技术的发展,计算机软件系统的复杂性越来越高,所涉及的代码量越来越大,同时程序中的错误和问题隐患也越来越多。因此,如何提高软件系统的可靠性和安全性已成为计算机软件领域的一个紧迫需求。软件模型检测技术是提高程序可靠性和安全性的重要途径。该技术可以自动化地验证程序是否可以满足一些关键性质。C语言是目前软件领域最为广泛使用的编程语言之一。它的语法规范比较灵活,尤其是对指针的使用,稍微不注意,就会导致程序崩溃。在C程序中,对指针的不正确使用,会带来如内存泄露,指针未初始化、多次释放,以及空指针解引用等问题。本文研究基于CEGAR技术的C程序空指针解引用的检测算法。首先,实现了基于CEGAR的C程序PPTL模型检测算法。在此基础上,通过PPTL公式来描述空指针解引用的特征,进一步检测C程序中是否存在空指针解引用的问题。为了提高验证的自动化水平,本文通过对C源代码进行扫描,对所涉及到的指针自动产生待验证的PPTL性质,避免了手动在C程序中加入断言所带来的麻烦。在以上方法的基础上,实现了基于CEGAR的C程序PPTL模型检测检测工具:PPTLChecker。该工具可以支持PPTL公式描述的程序性质的验证,实现了对程序中空指针解引用问题的自动化检测功能。实验结果表明,PPTLChecker在C程序空指针解引用检测中有着实际的应用价值。