一种验证指针程序的方法  

A method of verification pointer program

作　　者：张志天[1,2] 陈意云[1,2] 刘刚[1,2] 

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

出　　处：《微型机与应用》2011年第16期9-11,共3页Microcomputer & Its Applications

摘　　要：利用形状图逻辑和形状系统来解决指针程序的分析和验证中的困难。该方法要求程序员声明各种递归结构体类型参与构建的数据结构的形状,并声明指针变量所指向的形状,以便程序分析工具能建立各程序点的形状图,并以此来支持程序验证。探讨了在指针相等关系静态可确定的情况下,避免在Hoare逻辑上做复杂扩展的指针程序验证方法。Analysis and verification of programs dealing with pointers are still difficult problems so far. This paper uses a shape graph logic and a shape system to solve these problems. Using our method, programmers must declare the shapes that the recursive data structuresintend to build, and the shapes that pointer variables point to. Thus shape graphs can be constructed using an analysis tool and used tosupport the program verification. This paper presents a method for pointer program verification avoiding to make complicated extensions to Hoare logic in the situation that equalities over pointers can be decided statically.

关 键 词：HOARE逻辑 形状图逻辑 程序分析 分离逻辑 

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