| 一种验证指针程序的方法 |
| |
| 引用本文： | 张志天,陈意云,刘刚.一种验证指针程序的方法[J].微型机与应用,2011,30(16). |
| |
| 作者姓名： | 张志天 陈意云 刘刚 |
| |
| 作者单位： | 中国科学技术大学计算机科学与技术学院,合肥,230026 |
| |
| 摘 要： | 利用形状图逻辑和形状系统来解决指针程序的分析和验证中的困难。该方法要求程序员声明各种递归结构体类型参与构建的数据结构的形状，并声明指针变量所指向的形状，以便程序分析工具能建立各程序点的形状图，并以此来支持程序验证。探讨了在指针相等关系静态可确定的情况下，避免在Hoare逻辑上做复杂扩展的指针程序验证方法。Abstract：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
|
| 关 键 词： | Hoare逻辑 形状图逻辑 程序分析 分离逻辑 |
A method of verification pointer program |
| |
| Zhang Zhitian ,Chen Yiyun ,Liu Gang.A method of verification pointer program[J].Microcomputer & its Applications,2011,30(16). |
| |
| Authors: | Zhang Zhitian Chen Yiyun Liu Gang |
| |
| Affiliation: | Zhang Zhitian 1,2,Chen Yiyun 1,Liu Gang 1,2(1.School of Computer Science,University of Science and Technology of China,Hefei 230026,China,(2.Software Security Lab.,2.Suzhou Institute for Advanced Study,Suzhou 215123,China) |
| |
| Abstract: | 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 |
| |
| Keywords: | Hoare logic shape graph logic program analysis separation logic |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
