| 基于分离逻辑的程序分析技术 |
| |
| 引用本文： | 裴芳,刘云龙,张洁,郝丽波. 基于分离逻辑的程序分析技术[J]. 火力与指挥控制, 2012, 37(6): 63-67 |
| |
| 作者姓名： | 裴芳 刘云龙 张洁 郝丽波 |
| |
| 作者单位： | 1. 湖南机电职业技术学院,长沙,410073
2. 长沙开元仪器有限公司,长沙,410100 |
| |
| 基金项目： | 湖南省教育厅科学研究基金资助项目 |
| |
| 摘 要： | 分离逻辑是John C Reynolds和Peter O’Hearn于2000年提出的基于Hoare逻辑分析程序中动态分配内存和指针别名的逻辑理论。首先回顾了分离逻辑系统的理论框架,然后讨论了分离逻辑在程序分析领域中符号执行、形态分析和并发程序分析验证这些领域中的应用成果,最后介绍了分离逻辑在程序分析技术中当前主要的研究方向。
|
| 关 键 词： | 分离逻辑 程序分析 Hoare逻辑 形态分析 |
Study on Program Analysis Techniques Based on Separation Logic |
| |
| PEI Fang , LIU Yun-Long , ZHANG Jie , HAO Li-bo. Study on Program Analysis Techniques Based on Separation Logic[J]. Fire Control & Command Control, 2012, 37(6): 63-67 |
| |
| Authors: | PEI Fang LIU Yun-Long ZHANG Jie HAO Li-bo |
| |
| Affiliation: | 1(1.Hunan Mechanical&Electrical PolyTechnic,Changsha 410073,China,2.Changsha Kaiyuan Instruments Co.,LTD,Changsha 410100,China) |
| |
| Abstract: | The separation logic,as an extension of Hoare logic,is proposed by John C Reynolds and Peter O’ Hearn in 2000,and is widely used to analyze dynamic allocated memory and pointer alias in programs.This paper revisits the framework of separation logic,and then discusses some applications of separation logic in the fields,such as: symbolic execution,shape analysis and concurrent program verification.Consequently,the trend of separation logic is also briefly pointed out. |
| |
| Keywords: | separation logic program analysis hoare logic shape analysis |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
