软件测试是保证软件质量的必要手段。由于基于用例运行程序进行测试低效且容易出错，人们从六十年代起就开始探索用例测试之外的其它软件质量保证手段。程序验证尝试以严格的定理证明方式确保程序正确。然而由于程序设计语言的复杂性，程序验证只用于证明一些关键的核心模块的正确性，而没有得到更广泛的应用。程序静态测试是介于程序验证和基于用例的测试之间的方法。静态测试不编译运行程序，仅依据规约或者规则对源码进行分析以检测程序中是否存在错误。静态测试不能证明程序的完全正确，但是可以作为动态测试的补充。目前关于程序静态分析的研究是软件工程研究的一个热点。 对程序进行静态测试，首先需要分析理解程序的行为。指针变量和存储模型紧密相关，不能简单地作为数值型变量予以处理。分析包含指针变量的程序一直是静态测试中需要解决的一个难题。本文提出的变量关系图这一抽象模型，一方面用于抽象地描述了程序的存储结构，另一方面也描述变量间的约束关系。和其它已经提出的抽象模型相比，变量关系图能够更深刻地揭示程序中变量间的约束关系。 针对包含指针以及结构类型变量的程序路径，我们提出了以变量关系图为基础，结合符号执行对其进行分析的方法。在符号执行中根据程序动作调整变量关系图的结构，同时根据程序中的条件生成相应的约束条件集合。通过考察符号执行中生成的变量关系图，可以检测程序中悬空指针引用、存储泄漏以及变量未初始化等具有一般性的错误。此外，通过对符号执行后求得的约束集合进行求解，我们还可以检查和具体程序相关的错误。 具体实现方面，在已有的路径分析工具PAT的基础上进行了扩展，使之能够处理包含指针类型和结构类型变量。利用变量关系图和符号执行，我们可以精确地获取程序的存储模型及变量间约束关系的信息，可以发现一些已有的分析工具不能发现的错误。此外，我们设计一个小的规约语言并实现相应的翻译工具，使得能够较为简洁地描述程序的规约。