Scholarlink

<p>We devise a direct decision procedure to test entailment in a separation logic of relations, which generalizes standard separation logic by considering structures defined over arbitrary relations. The logic allows for user-defined predicate symbols, describing structures of unbounded size, with a fixpoint semantics. We show that the entailment problem is 2-<span>ExpTime</span> complete if the rules defining the semantics of these predicates satisfy some conditions, which generalize the PCE conditions of Iosif et al. (in: Proceedings of CADE-24, Volume 7898 of LNCS, 2013).</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

A Direct Procedure to Test Entailment in a Separation Logic of Relations

  • 期刊论文

  • 发表日期：

    2025年5月3日

查看全文
  • Mnacho Echenim,
  • Nicolas Peltier

摘要

We devise a direct decision procedure to test entailment in a separation logic of relations, which generalizes standard separation logic by considering structures defined over arbitrary relations. The logic allows for user-defined predicate symbols, describing structures of unbounded size, with a fixpoint semantics. We show that the entailment problem is 2-ExpTime complete if the rules defining the semantics of these predicates satisfy some conditions, which generalize the PCE conditions of Iosif et al. (in: Proceedings of CADE-24, Volume 7898 of LNCS, 2013).