基于分离逻辑的程序分析技术  

Study on Program Analysis Techniques Based on Separation Logic

作　　者：裴芳[1] 刘云龙 张洁[1] 郝丽波[1] 

机构地区：[1]湖南机电职业技术学院,长沙410073 [2]长沙开元仪器有限公司,长沙410100

出　　处：《火力与指挥控制》2012年第6期63-67,共5页Fire Control & Command Control

基　　金：湖南省教育厅科学研究基金资助项目(10C0152)

摘　　要：分离逻辑是John C Reynolds和Peter O'Hearn于2000年提出的基于Hoare逻辑分析程序中动态分配内存和指针别名的逻辑理论。首先回顾了分离逻辑系统的理论框架,然后讨论了分离逻辑在程序分析领域中符号执行、形态分析和并发程序分析验证这些领域中的应用成果,最后介绍了分离逻辑在程序分析技术中当前主要的研究方向。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.

关 键 词：分离逻辑 程序分析 HOARE逻辑 形态分析 

分 类 号：TP31[自动化与计算机技术—计算机软件与理论]