计算机系统已在国防、通讯、金融、能源、交通、医疗等关键领域中得到广泛应用,构建高可信系统已成为世界范围的重要课题。其中操作系统内核的安全可靠性是构建高可信计算机系统的关键,任何一个微小的内核错误都有可能导致整个计算机系统崩溃。形式化程序验证是使用逻辑推理系统来保证计算机程序的正确性,对于规模相对较小而设计复杂的内核程序而言,它是保证其安全可靠的有效方法之一。底层的系统软件大都采用C语言编写,而C程序中的指针操作和系统软件中数据结构间复杂的逻辑关系,使得验证系统软件的程序逻辑的断言语言需要具有足够的表达能力。然而,具有足够表达力的断言语言推理的不可判定性导致推理验证的过程无法完全自动化,而手动验证系统软件需要耗费大量的人力和物力。因此,如何在不牺牲逻辑断言的表达力的前提下,尽可能的提高C程序的验证效率是一个亟待解决的问题。本文通过开发证明策略来提高C程序在定理证明工具Coq中的验证效率。由于人工交互的手动证明在验证复杂系统软件中不可避免,因此在提供自动化支持的过程中同时需要兼顾以下两个方面：一方面,需要尽可能的减少手动证明的工作量；另一方面,当证明策略失败时,能够产生对用户有用的出错提示信息,这样用户可以根据提示信息快速地定位问题所在,或者手动证明那些无法自动证明的命题,或者通过调整规范或代码来完成证明。基于上述考虑,本文开发了一组C程序的实用证明策略,包括自动证明分离逻辑断言之间蕴含关系的证明策略和自动产生验证条件并证明Hoare三元组的证明策略,它们同时兼顾验证效率和易用性。本文工作的主要贡献如下：·本文将数据结构形状相关的领域专用知识(譬如单链表)引入到证明策略的实现中,并对相关归纳谓词做自动展开来减少手动证明的工作量,从而提高C程序的验证效率。·本文通过在证明策略中引入预处理阶段来反馈出错提示信息帮助用户定位自动证明失败的问题所在,这在进行人工交互式证明时极大地提高了证明策略的可用性和易用性。·本文根据上述两个想法在定理证明工具Coq中实现了一组C程序证明策略(约一万行Coq代码),它们能用于全自动的验证一些简单的操作单链表的C程序。