题目：基于懒符号执行的程序模型检查器

飞行器、核反应设施等安全性要求极高的系统中，对软件的验证有更严格的要求。作为传统验证技术的补充，静态分析、运行时监控和模型检查可以提高软件的可靠性、降低开发成本。本文是将传统模型检查技术应用于程序错误发现的一次探索，研究针对实际程序设计语言(C语言)的程序模型检查技术。模型检查一个实际程序是相当困难的。与传统模型检查器的建模语言相比，实际程序设计语言的结构更为复杂，而多数模型检查工具中使用某种逻辑形式系统描述程序性质，程序员难以理解和掌握。最大的挑战是如何解决状态空间爆炸问题，通常可以认为一般程序的状态空间是无限的。针对上述问题，本文提出了一个基于懒符号执行的程序模型检查器框架，即：通过系统地遍历和符号执行程序的控制流路径，计算程序的状态空间，用断言和状态机描述检查性质，在程序的符号状态和具体状态上分别检查断言和状态机性质。文中着重解决了该程序模型检查框架实现中的关键技术：1. 提出了基于懒替换的符号执行方法，较好地解决了传统符号执行中的动态地址计算和库函数问题。懒符号执行采取尽可能替换的策略，满足符号执行条件时才执行，否则就不执行而是保留原来的变量。2. 提出了多层次的约束求解方法，解决了含中间变量状态约束的求解问题。通过对状态约束的化简，快速排除具有某些特征的不可行状态，以缓解路径爆炸的问题。对于不能快速排除的状态，利用静态技术求解状态约束中的输入约束，并结合动态求解机制求解其中的中间约束。3. 扩展了C语言以支持断言和状态机描述，设计了断言和状态机的模型检查算法。在C语言中增加了检查片断、断言和状态机等语言结构，同时支持局部性质和全局性质的表示。本文初步实现了一个面向C程序的程序模型检查器CMC(the C Model Checker)的原型，并进行了一系列实验，初步实验表明了CMC的可行性。本质上，模型检查等于穷尽测试。从程序测试的角度看，CMC是一个以路径覆盖为测试准则的单元测试工具，由于在被测试程序中插装了检查性质，CMC可以自动地检测出违反性质的错误，提高了测试效率。