在社会高度信息化的今天,社会生产生活高度依赖软件系统,因此软件系统的安全性与可靠性也就显得愈加重要,通过形式化验证的方式保证程序的安全是一种重要的手段。形式化验证有两种方法,一种是模型检测,模型检测能够通过遍历系统所有的状态空间,自动验证有穷状态的系统并构造不满足性质定理的反例。另一种是演绎推理,它使用形式化的方式对程序进行数学推理,尽管以这种方式实现的自动验证工具早已有实验室开发出来,但是至今都无法在工业界使用。究其原因在于自动定理证明方面的困难,因为不管是断言语言描述能力的提升、循环不变式的推断、别名判断和验证条件的证明等,最终还是受到自动定理证明器能力的影响。鉴于这些原因,在研究自动定理证明的同时,应当适当考虑降低对自动定理证明期待,可以通过设计安全的语言去提高合法程序的门槛,同时设计规范语言来描述程序代码的行为性质以降低定理证明器的负担。本文主要贡献：第一,设计了一种面向验证的C语言子集,称为安全C语言。在基于HOare逻辑推理规则对程序进行形式验证过程中,每当使用赋值公理{Q[E/x])x=E{Q}(Q是赋值语句的后断言,Q[E/x]表示对Q中所有x代换为E)时,必须保证后断言Q与赋值语句x=E中没有潜在别名,否则Q[E/x]是最弱前断言的结论不可靠,而C语言广泛存在的别名,给基于Hoare逻辑的推理带来难题。本文在基于C99标准之上,从别名的角度讨论了C语言的安全性以及其会给程序验证带来的问题,并以此为启示设计了安全C语言,在安全C语言中要求对C语言中各种类型增加编程限制来使得对这些被限制类型的变量操作表现得较为规范,同时还要求使用标注对程序加以说明以减轻定理证明器负担。第二,设计了一种规范语言,规范语言定义了安全C语言要求的标注的语法语义及使用方式,规范语言以形式化的方式描述C程序的行为性质,这些对C程序行为性质的描述最终都会传递给自动定理证明器,从而更大程度上帮助自动定理证明器认知程序的行为,并最终验证程序行为是否符合规范中的描述。在规范语言中还专门引入形状描述来表示指针相关性质,以解决指针引起的别名导致程序难以验证这一问题。第三,基于clang实现了安全C语言要求的编程约束检查以及规范语言的分析。