一句话：提出首个支持堆操作程序中任意量词交替超属性模块化推理的程序逻辑 HSL。
非干涉、确定性、广义非干涉（GNI）等是关联多次执行的超属性。现有分离逻辑只支持特定类别，如 ∀∀ 的非干涉或 ∃∃ 的非确定性，无法表达需量词交替的 GNI；唯一支持任意量词交替的 Hyper Hoare Logic 不能处理堆操作程序。本文提出超分离逻辑（HSL），首个面向堆操作程序、支持任意量词交替超属性模块化推理的程序逻辑。HSL 将 Hyper Hoare Logic 与新的超分离合取结合，把标准分离合取提升到状态集合上，从而给出超属性的广义框架规则。作者在 Isabelle/HOL 中证明 HSL 可靠，并展示其表达力超出既有分离逻辑。
Many important functional and security properties—including non-interference, determinism, and generalized non-interference (GNI)—are hyperproperties, i.e., properties relating multiple executions of a program. Existing separation logics allow one to reason about specific classes of hyperproperties, e.g., ∀∀-hyperproperties such as non-interference and ∃∃-properties such as non-determinism. However, they do not support quantifier alternation, which is for instance needed to express GNI. The only existing logic that can reason about such properties is Hyper Hoare Logic, but it does not support heap-manipulating programs and, thus, is not applicable to common imperative programs. This paper introduces Hyper Separation Logic (HSL), the first program logic that supports modular reasoning about hyperproperties with arbitrary quantifier alternation over programs that manipulate the heap. HSL generalizes Hyper Hoare Logic with a novel hyper separating conjunction that lifts the standard separating conjunction to sets of states, enabling a generalized frame rule for hyperproperties. We prove HSL sound in Isabelle/HOL and demonstrate its expressiveness for hyperproperties that lie beyond the reach of existing separation logics.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{GospodinovMD26,
title = {Hyper Separation Logic},
author = {Trayan Gospodinov and Peter Müller and Thibault Dardinier},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808328}
}