| 循环不变形状图的自动推断 |
| |
| 引用本文： | 刘刚,陈意云,张志天.循环不变形状图的自动推断[J].电子技术,2011,38(8):4-6. |
| |
| 作者姓名： | 刘刚 陈意云 张志天 |
| |
| 作者单位： | 1. 中国科学技术大学计算机科学与技术学院
2. 中国科学技术大学苏州研究院软件安全实验室 |
| |
| 摘 要： | 在指针程序的分析和验证过程中,循环不变式的自动推断一直是个研究热点.文章首先介绍所提出的形状图和形状图逻辑,形状图逻辑是一种把形状图看成有关指针的断言,并在此基础上对Hoare逻辑进行扩展而得到的程序逻辑.然后在此基础之上,设计了一种基于形状图逻辑的形状分析方法,并提出了一种基于形状图逻辑的循环不变形状图的推断方法.
|
| 关 键 词： | 形状图逻辑 循环不变式 程序验证 形状分析 |
Automatic Inference of Loop-Invariant Shape Graphs |
| |
| Liu Gang,Chen Yiyun,Zhang Zhitian.Automatic Inference of Loop-Invariant Shape Graphs[J].Electronic Technology,2011,38(8):4-6. |
| |
| Authors: | Liu Gang Chen Yiyun Zhang Zhitian |
| |
| Affiliation: | Liu Gang Chen Yiyun Zhang Zhitian(1.School of Computer Science,University of Science and Technology of China 2.Software Security Lab.,Suzhou Institute for Advanced Study,University of Science and Technology of China) |
| |
| Abstract: | Automatic inference of Loop-Invariant has been a hot research topic in the field of analysis and verification of pointer programs.In this paper,we first describe the proposed shape graph and shape graph logic,the shape graph logic is an extension to Hoare logic by regarding shape graphs as assertions about pointers directly.Then based on the shape graph logic,we design a method for shape analysis on pointer programs and after that we put forward a method for inferring loop invariant shape graphs associated ... |
| |
| Keywords: | shape graph logic loop invariant program verification shape analysis |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
