提高程序验证自动化程度的技术

项目名称： 提高程序验证自动化程度的技术

项目编号： No.61170018

项目类型： 面上项目

立项/批准年度： 2012

项目学科： 计算机科学学科

项目作者： 陈意云

作者单位： 中国科学技术大学

项目金额： 56万元

中文摘要： 基于逻辑推理的程序验证是提高软件可信程度的一种重要方法。本项目研究促进程序验证方法走向实用的技术和相关理论，重点解决指针类型给程序验证带来的障碍，为指针程序的自动验证设计一种比较全面的解决办法。 该项研究基于下面的思路：（1）程序验证不必孤立地进行，可用程序分析收集的信息来支持程序验证；（2）程序员可通过提供一些对程序分析和程序验证有用的提示，来换取它们替程序员完成一些很有价值的事情；（3）在通过增强编程语言和断言语言的表达能力来拓展程序验证器的能力时，要尽量避免给自动定理证明器带来太多的负担。 本项目的研究基于上面的思路展开，预计主要亮点是：提出一种直接把形状图作为断言的形状图逻辑，提出形状系统概念。 本项目的研究帮助解决程序自动验证的瓶颈问题，促进程序验证的研究和应用的开展。

中文关键词： 程序验证；程序分析；可信软件；程序逻辑；循环不变式推断

英文摘要：

英文关键词： program verification；program analysis；dependable software；program logic；inference of loop invariants