| 摘要: |
| 本文改进并扩展先前为验证指针程序提出的指针逻辑,主要贡献是提出了合法访问路径集合的概念,极大地简化了访问路径上的基本运算,并使得指针逻辑推理规则变得易理解.另外,增加了局部推理规则和函数构造的推理规则,使得指针逻辑可以方便地用于有函数调用的场合. |
| 关键词: 软件安全 Hoare逻辑 指针逻辑 携带证明的代码 出具证明的编译器 |
| DOI： |
| 分类号: |
| 基金项目:Supported by the National Natural Science Foundation of China under Grant Nos.90718026, 60928004 (国家自然科学基金) |
|
| Pointer Logic for Verification of Pointer Programs |
|
CHEN Yi-Yun,LI Zhao-Peng,WANG Zhi-Fang,HUA Bao-Jian
|
| Abstract: |
| 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. |
| Key words: software safety Hoare logic pointer logic proof-carrying code certifying compiler |
