断言语言支持自定义谓词的程序验证器原型

• 作者: 徐文义 李兆鹏 陈意云
• 来源期刊: 小型微型计算机系统
• 学科: 工学
• 关键词: 程序验证 Hoare逻辑 形状图逻辑 程序分析 自定义谓词
• 年，卷（期）: 2013,（7）
• 所属期刊栏目: 计算机软件与数据库研究
• 页码范围: 1482-1486
• 页数: 5页
• 分类号: TP311
• 字数: 8121字
• 语种: 中文

摘要

基于逻辑推理的方法进行程序验证是形式化程序验证的研究热点.目前的自动验证工具为了保证自动性,对描述程序性质的断言语言都有较多限制,导致程序的某些递归性质难以用断言语言表述.本文在一个面向指针程序、基于先前自行设计的形状图逻辑、依赖于自动定理证明工具Z3的自动程序验证原型系统上,通过在断言语言中引入自定义谓词来增强断言语言的表达能力,使得该原型系统不仅能自动验证含操作易变数据结构的程序的性质,也能自动验证一些不含指针的程序的性质.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陈意云	中国科学技术大学计算机科学与技术学院	83	854	16.0	26.0
5	李兆鹏	中国科学技术大学计算机科学与技术学院	17	99	7.0	9.0
9	徐文义	中国科学技术大学计算机科学与技术学院	1	3	1.0	1.0