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

Study on Program Analysis Techniques Based on Separation Logic

分离逻辑是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.