火力与指挥控制2012，Vol.37Issue(6)：63-67,5.
基于分离逻辑的程序分析技术
Study on Program Analysis Techniques Based on Separation Logic
摘要
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.关键词
分离逻辑/程序分析/Hoare逻辑/形态分析Key words
separation logic/program analysis/hoare logic/shape analysis分类
信息技术与安全科学引用本文复制引用
裴芳,刘云龙,张洁,郝丽波..基于分离逻辑的程序分析技术[J].火力与指挥控制,2012,37(6):63-67,5.基金项目
湖南省教育厅科学研究基金资助项目(10C0152) （10C0152）
