随着计算机技术的快速发展,计算机软件的规模越来越大,软件调试和维护越来越困难,其成本也越来越高,软件的安全形势变得越来越重要。特别是在安全攸关领域(例如,航空航天、高铁、核电、医疗等领域),人们对高可信软件的需求越来越大。在这些领域,C语言仍是最普遍使用的编程语言。而C程序中的空指针脱引用、内存泄漏、缓冲区溢出等诸多内存安全问题在软件开发中依然突出。提高软件质量的方法有很多种,如软件测试、程序分析和程序验证等；在众多方法中,相对有效而又经济的方法是程序静态分析。针对C程序中内存安全问题,作者所在实验室的课题组开发了一个静态分析工具,该工具采用了符号执行的静态分析技术,并加入了形状分析,为了降低静态分析的误报率和漏报率,以及提高分析的效率,设计了表达能力较为丰富的规范语言来描述程序状态和函数行为。在该静态分析工具的实现中,设计了描述函数行为的规范语言,包括描述程序状态的基本断言,描述内存状态的谓词以及描述单链表、双链表、二叉树的形状谓词。该工具基于编译框架LLVM和符号执行分析工具KLEE,以函数为单位分析并构造函数行为规范,该过程中需要用断言描述程序状态并按需抽象成形状谓词。为此,针对断言设计了一系列的规范化和抽象化规则。本文的贡献主要有三方面：第一,设计并实现了描述函数行为的规范语言,包括描述程序状态的基本断言,描述内存的谓词以及描述单链表、双链表、二叉树的形状谓词。通过规范语言来记录已分析函数的行为,可以避免重复分析,提高分析的效率。通过使用描述内存的谓词和形状谓词,该工具可以检测内存泄漏、空指针脱引用等内存安全问题以及进行形状分析。第二,设计并实现了一系列的规则来规范和抽象断言,将程序状态抽象成形状谓词,用于形状分析。第三,利用已有的规范语言为C语言标准库函数构造函数行为规范。许多程序中会频繁调用C的库函数,为这些常用的库函数手动构造行为规范可以提高分析的精度和效率。本文工作的意义在于针对C程序内存安全问题,提出了一套规范语言；并针对形状分析,提出了一系列的抽象化规则,用于精确分析单链表、双链表和二叉树等递归数据结构程序中的内存安全错误,为以后的研究和工具扩展奠定了基础。