东篱科研大数据发现系统（DRDS）

位置：成果数据库 > 期刊 > 期刊详情页

一种用于指针程序验证的指针逻辑

期刊名称：软件学报, 21(3), pp 415-426, 2010/3.(EI收录)
时间：0
分类：TP301[自动化与计算机技术—计算机系统结构;自动化与计算机技术—计算机科学与技术]
作者机构：[1]中国科学技术大学计算机科学与技术学院,安徽合肥230026, [2]中国科学技术大学苏州研究院软件安全实验室,江苏苏州215123
相关基金：Supported by the National Natural Science Foundation of China under Grant Nos.90718026, 60928004 （国家自然科学基金）
相关项目：高可信软件中的形式程序验证

关键词：软件安全, HOARE逻辑, 指针逻辑, 携带证明的代码, 出具证明的编译器, software safety, Hoare logic, pointer logic, proof-carrying code, certifying compiler

中文摘要：

本文改进并扩展先前为验证指针程序提出的指针逻辑，主要贡献是提出了合法访问路径集合的概念，极大地简化了访问路径上的基本运算，并使得指针逻辑推理规则变得易理解．另外，增加了局部推理规则和函数构造的推理规则，使得指针逻辑可以方便地用于有函数调用的场合．

英文摘要：

This paper improves and extends the pointer logic that has been designed for verifying pointer programs. Its main contribution is that a concept of legal sets of access paths is presented, which simplifies elementary operations on access paths and makes inference rules of the logic easier to understand. Furthermore, the logic with inference rules is ＇extended for local reasoning and for function construction, making the logic used conveniently in the context of function calls.

同期刊论文项目