论文标题
强分离逻辑
Strong-Separation Logic
论文作者
论文摘要
用于分离逻辑的大多数自动化验证者目标符号片段片段，既不允许魔术运算符和经典布尔操作员在空间公式中的应用。这并不奇怪，因为对魔术棒的支撑很快导致了不可证明的性能，尤其是在与归纳性谓词相结合以进行数据结构的推理时。为了避免这些不可证明的结果，我们建议将更加限制的语义分配给分离的连词。我们认为，所得的逻辑，强分离逻辑可用于组成程序验证和Bi-by-by-by-by-by-by-by-by-by-by静态分析，就像“标准”分离逻辑一样，同时即使在魔术棒和列表段谓词存在的情况下仍然可以决定 - 假设具有不可渗透性的功能的组合，则可以假设具有标准语义的能力。
Most automated verifiers for separation logic target the symbolic-heap fragment, disallowing both the magic-wand operator and the application of classical Boolean operators to spatial formulas. This is not surprising, as support for the magic wand quickly leads to undecidability, especially when combined with inductive predicates for reasoning about data structures. To circumvent these undecidability results, we propose to assign a more restrictive semantics to the separating conjunction. We argue that the resulting logic, strong-separation logic, can be used for compositional program verification and bi-abductive static analysis just like "standard" separation logic, while remaining decidable even in the presence of both the magic wand and the list-segment predicate -- a combination of features that leads to undecidability assuming the standard semantics.
