交通、电力、军事等关键领域对软件的可靠性和安全性要求越来越高，因为其严重关乎国民的人身和财产安全。C语言在上述基础领域软件的开发中有广泛的应用。C语言灵活高效的特性允许程序员做相当底层的操作，但也导致C程序容易出现非法指针解引用、内存泄漏、缓冲区溢出等缺陷。　　形式化验证是一种可以严格保证程序可靠性的方法。本课题组正在研发一个安全C语言验证器，其功能是对携有程序标注的安全C语言程序进行演绎推理，验证程序是否满足预期规范。　　安全C语言验证器中验证条件生成器的作用是支持安全C语言和规范语言SCSL的语法，实现每条语句的演算规则，并根据演算规则遍历源程序进行演算，同时产生程序点的断言和合理有效的验证条件。本文的工作是对安全C语言验证器中的验证条件生成器进行扩展。　　本文的主要工作和贡献如下:　　第一、参与规范语言SCSL中逻辑变量、幽灵代码、字符串类型、带命名行为协议和多函数协议的设计，提高了规范语言的表达能力，同时独立设计和实现了对应的演算规则。　　第二、基于Hoare逻辑设计和实现跳转语句goto、continue和break、选择语句switch以及函数调用语句的演算规则，使得验证器可以支持更多C的语法和控制结构，扩大了验证器的适用范围。同时实现了赋值语句前对全称量化断言和谓词的展开，减轻了自动定理证明器的负担。　　第三、根据C语言的语义提出了一种适用于程序验证的栈区内存模型，可以支持结构体和多级指针等数据类型，并基于该模型实现了取地址、多级解引用和指针关系运算等操作的演算规则。同时基于该模型提出了一种判断别名的算法，能够在应用Hoare赋值规则前准确完成别名替换。　　经过上述扩展设计与实现，提高了安全C语言验证器的证明能力和可用性。目前已经成功验证多例C程序，其中包括快速排序、冒泡排序、字符串匹配等经典算法。