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

Verifier Prototype for Programs with User-defined Predicates in the Assertion Language

作　　者：徐文义[1,2] 陈意云[1,2] 李兆鹏[1,2] 

机构地区：[1]中国科学技术大学计算机科学与技术学院,合肥230026 [2]中国科学技术大学苏州研究院软件安全实验室,江苏苏州215123

出　　处：《小型微型计算机系统》2013年第7期1482-1486,共5页Journal of Chinese Computer Systems

基　　金：国家自然科学基金项目(61003043;61170018)资助

摘　　要：基于逻辑推理的方法进行程序验证是形式化程序验证的研究热点.目前的自动验证工具为了保证自动性,对描述程序性质的断言语言都有较多限制,导致程序的某些递归性质难以用断言语言表述.本文在一个面向指针程序、基于先前自行设计的形状图逻辑、依赖于自动定理证明工具Z3的自动程序验证原型系统上,通过在断言语言中引入自定义谓词来增强断言语言的表达能力,使得该原型系统不仅能自动验证含操作易变数据结构的程序的性质,也能自动验证一些不含指针的程序的性质.The automatic program verification based on logical reasoning for program properties is currently a research focus.In the automatic verification system,there are a lot of limitations on the pow er of assertion languages,therefore some recursive properties are difficult to describe.This paper presents a method to enhance the pow er of assertion language by introducing user-defined predicates.Our verifier supports properties of the programs w ith and w ithout modifiable data structures.

关 键 词：程序验证 HOARE逻辑 形状图逻辑 程序分析 自定义谓词 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]