Translating Separation Logic into a Fragment of the First-Order Logic

摘要：

Separation logic is an extension of Hoare logic for reasoning about mutable heap structure. To represent separation logic in the first-order logic, there are several choices to determine what are constants, what are predicates and quantifiers, and whether the commands are taken as atomic or composite. This paper shall give a translation of separation logic into a guarded fragment of the first-order logic, such that the translation is faithful, that is, the translation translates a consistent statement (boolean expression, assertion or specification) of separation logic into a consistent formula in the fragment of the first-order logic. By the decidability of the satisfiability problem of the guarded first-order logic, if the commands are taken as atomic in the first-order logic then the guarded first-order logic translated from separation logic is decidable; if the commands are taken as atomic/composite in the first-order logic then the first-order logic translated from separation logic is undecidable.

作者: Yuefei Sui Yuming Shen Cungen Cao Ju Wang

作者单位: Key Laboratory of Intelligent Information Processing, Institute of Computing Technology, Chinese Aca Key Laboratory of Intelligent Information Processing, Institute of Computing Technology, Chinese Aca School of Computer Science and Information Engineering, Guangxi Normal University Guilin China 54100

会议类型: 国际会议

会议名称: Sixth International Conference on Semantics,Knowledge and Grids(第六届语义、知识与网格国际会议 SKG 2010)

会议地点: 宁波

会议语种:英文

页码: 188-194

在线出版日期: 2010-11-01（万方平台首次上网日期，不代表论文的发表时间）