pith. machine review for the scientific record. sign in

arxiv: 2604.12870 · v2 · submitted 2026-04-14 · 💻 cs.PL

Recognition: unknown

Hyper Separation Logic (extended version)

Peter M\"uller, Thibault Dardinier, Trayan Gospodinov

Authors on Pith no claims yet

Pith reviewed 2026-05-10 13:39 UTC · model grok-4.3

classification 💻 cs.PL
keywords hyper separation logichyperpropertiesseparation logicquantifier alternationheap manipulationprogram verificationmodular reasoninggeneralized non-interference
0
0 comments X

The pith

Hyper Separation Logic is the first to support modular reasoning about hyperproperties with arbitrary quantifier alternation for heap-manipulating programs.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents Hyper Separation Logic to let programmers prove properties that relate several executions of a program, including cases where quantifiers alternate such as generalized non-interference. Prior separation logics could handle uniform quantifiers like non-interference or non-determinism but not mixed ones, while the one logic that supported alternation did not apply to programs that use heaps. The new logic adds a hyper separating conjunction that works on sets of states rather than single states, which produces a generalized frame rule that stays sound even when executions allocate and access memory. This matters for verifying security and correctness in ordinary imperative code that combines mutable state with multi-execution requirements.

Core claim

Hyper Separation Logic (HSL) generalizes Hyper Hoare Logic by introducing a hyper separating conjunction that lifts the standard separating conjunction to sets of states. This lifting yields a generalized frame rule that preserves soundness for hyperproperties with arbitrary quantifier alternation over programs that manipulate the heap. The paper proves HSL sound in Isabelle/HOL and shows that it can express hyperproperties beyond the reach of earlier separation logics.

What carries the argument

The hyper separating conjunction, which lifts the standard separating conjunction from single states to sets of states and thereby supports a sound generalized frame rule for hyperproperties.

If this is right

  • Allows modular proofs of generalized non-interference for imperative programs that allocate and access the heap.
  • Supports hyperproperties using any combination of universal and existential quantifiers over multiple executions.
  • Preserves the frame rule when reasoning about resources shared or separated across those executions.
  • Applies directly to common imperative languages with mutable memory.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same lifting technique could be tried on other resource logics that currently lack hyperproperty support.
  • It may enable embedding HSL rules into existing automated verifiers for languages with pointers.
  • Similar set-based extensions might help connect separation logic to model checkers that already handle hyperproperties.

Load-bearing premise

The hyper separating conjunction must be defined so that it correctly extends the standard one to sets of states without breaking the soundness of the generalized frame rule when programs modify the heap.

What would settle it

A concrete heap-manipulating program together with a hyperproperty that uses quantifier alternation for which HSL derives an incorrect judgment would falsify the claim.

Figures

Figures reproduced from arXiv: 2604.12870 by Peter M\"uller, Thibault Dardinier, Trayan Gospodinov.

Figure 1
Figure 1. Figure 1: Local reasoning with hyper-triples. The proof contains two applications of our generalized frame rule, [PITH_FULL_IMAGE:figures/full_fig_p006_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Illustrations of two applications of the hyper separating conjunction. Circular sectors denote the heap [PITH_FULL_IMAGE:figures/full_fig_p008_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Illustration of the problem of non-local errors. [PITH_FULL_IMAGE:figures/full_fig_p012_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Selected Rules of Hyper Separation Logic. [PITH_FULL_IMAGE:figures/full_fig_p017_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Proof outline showing that the program in black violates GNI, where the high input is stored at location [PITH_FULL_IMAGE:figures/full_fig_p020_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Proof that the program in black satisfies GNI, with the (unaltered) [PITH_FULL_IMAGE:figures/full_fig_p020_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Small-step semantics of program commands, where [PITH_FULL_IMAGE:figures/full_fig_p025_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Definition of modified variables (md) for program commands. [PITH_FULL_IMAGE:figures/full_fig_p026_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Additional rules of Hyper Separation Logic. [PITH_FULL_IMAGE:figures/full_fig_p028_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Proof that the program in black encounters an error caused by freeing aliased memory. [PITH_FULL_IMAGE:figures/full_fig_p031_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Proof that the program in black satisfies monotonicity. [PITH_FULL_IMAGE:figures/full_fig_p031_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: Proof that the program in black satisfies non-interference. [PITH_FULL_IMAGE:figures/full_fig_p032_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: Proof that the program in black exhibits non-determinism. [PITH_FULL_IMAGE:figures/full_fig_p032_13.png] view at source ↗
Figure 14
Figure 14. Figure 14: Proof that, when the program in black is executed from a non-empty [PITH_FULL_IMAGE:figures/full_fig_p033_14.png] view at source ↗
read the original abstract

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., $\forall\forall$-hyperproperties such as non-interference and $\exists\exists$-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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The paper introduces Hyper Separation Logic (HSL), the first program logic supporting modular reasoning about hyperproperties with arbitrary quantifier alternation (e.g., generalized non-interference) over heap-manipulating programs. It generalizes Hyper Hoare Logic via a novel hyper separating conjunction that lifts the standard separating conjunction to sets of states, yielding a generalized frame rule. Soundness is established via a machine-checked proof in Isabelle/HOL, and expressiveness is demonstrated for hyperproperties beyond the reach of prior separation logics limited to ∀∀ or ∃∃ cases.

Significance. If the soundness result holds, the work is significant: it closes the gap between separation logics (which handle heaps but only specific hyperproperties) and Hyper Hoare Logic (which handles quantifier alternation but not heaps). The machine-checked Isabelle/HOL proof for the hyper separating conjunction and generalized frame rule is a clear strength, providing direct verification of the central lifting construction rather than an unverified claim. This enables modular verification of important security and functional hyperproperties in realistic imperative code with dynamic memory.

minor comments (3)
  1. [§3.1] §3.1, Definition 3.3: the inductive definition of the hyper separating conjunction would benefit from an immediate concrete example (e.g., two singleton state sets) to illustrate how heap disjointness is lifted to sets of states.
  2. [§4.2] §4.2, Theorem 4.1 (generalized frame rule): the proof sketch references the Isabelle lemma but does not list the exact lemma name or theory file; adding this would aid reproducibility.
  3. [Figure 2] Figure 2 (expressiveness example for GNI): the diagram omits explicit quantifier labels on the execution traces, making it harder to see the alternation at a glance.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary and significance assessment of Hyper Separation Logic, as well as the recommendation for minor revision. No specific major comments were raised in the report.

Circularity Check

0 steps flagged

No significant circularity; machine-checked proof supplies independent support

full rationale

The paper defines a novel hyper separating conjunction that lifts standard separation to sets of states and proves a generalized frame rule sound for arbitrary quantifier alternation over heap programs. Soundness is established via a machine-checked Isabelle/HOL development supplied in the paper itself, satisfying the criterion for independent evidence. No step reduces by construction to a fitted parameter, self-definition, or load-bearing self-citation chain; the central claims remain externally falsifiable through the formalization rather than being renamed or presupposed inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The logic extends standard separation logic and Hyper Hoare Logic; the main addition is one new connective whose semantics and rules are defined and proven within the paper.

axioms (2)
  • domain assumption Standard separation logic axioms and rules for heap-manipulating programs
    HSL is presented as a generalization of existing separation logic.
  • domain assumption Semantics of hyperproperties and quantifier alternation over program executions
    Drawn from prior literature on hyperproperties and Hyper Hoare Logic.
invented entities (1)
  • hyper separating conjunction no independent evidence
    purpose: Lifts the standard separating conjunction to sets of states to enable modular reasoning about hyperproperties
    Newly introduced operator whose properties are defined and proven in the paper.

pith-pipeline@v0.9.0 · 5501 in / 1492 out tokens · 59085 ms · 2026-05-10T13:39:41.129201+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

37 extracted references · 32 canonical work pages

  1. [1]

    Naumann, and Minh Ngo

    Timos Antonopoulos, Eric Koskinen, Ton Chanh Le, Ramana Nagasamudram, David A. Naumann, and Minh Ngo. 2023. An Algebra of Alignment for Relational Verification.Proc. ACM Program. Lang.7, POPL (Jan. 2023), 20:573–20:603. doi:10.1145/3571213

    work page doi:10.1145/3571213 2023

  2. [2]

    Flavio Ascari, Roberto Bruni, Roberta Gori, and Francesco Logozzo. 2024. Sufficient Incorrectness Logic: SIL and Separation SIL. arXiv:2310.18156 [cs] doi:10.48550/arXiv.2310.18156

    work page doi:10.48550/arxiv.2310.18156 2024

  3. [3]

    Flavio Ascari, Roberto Bruni, Roberta Gori, and Francesco Logozzo. 2025. Revealing Sources of (Memory) Errors via Backward Analysis.Proc. ACM Program. Lang.9, OOPSLA1 (April 2025), 1321–1348. doi:10.1145/3720486

    work page doi:10.1145/3720486 2025

  4. [4]

    Nick Benton. 2004. Simple Relational Correctness Proofs for Static Analyses and Program Transformations. InProceed- ings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’04). Association for Computing Machinery, New York, NY, USA, 14–25. doi:10.1145/964001.964003

    work page doi:10.1145/964001.964003 2004

  5. [5]

    Raven Beutner. 2024. Automated Software Verification of Hyperliveness. InTools and Algorithms for the Construction and Analysis of Systems, Bernd Finkbeiner and Laura Kovács (Eds.). Springer Nature Switzerland, Cham, 196–216. doi:10.1007/978-3-031-57249-4_10

    work page doi:10.1007/978-3-031-57249-4_10 2024

  6. [6]

    Lars Birkedal, Bernhard Reus, Jan Schwinghammer, and Hongseok Yang. 2008. A Simple Model of Separation Logic for Higher-Order Store. InAutomata, Languages and Programming, Luca Aceto, Ivan Damgård, Leslie Ann Goldberg, Magnús M. Halldórsson, Anna Ingólfsdóttir, and Igor Walukiewicz (Eds.). Springer, Berlin, Heidelberg, 348–360. doi:10.1007/978-3-540-70583-3_29

    work page doi:10.1007/978-3-540-70583-3_29 2008

  7. [7]

    Arthur Charguéraud. 2020. Separation Logic for Sequential Programs (Functional Pearl).Proc. ACM Program. Lang.4, ICFP (Aug. 2020), 1–34. doi:10.1145/3408998

    work page doi:10.1145/3408998 2020

  8. [8]

    Clarkson and Fred B

    Michael R. Clarkson and Fred B. Schneider. 2008. Hyperproperties. In2008 21st IEEE Computer Security Foundations Symposium. 51–65. doi:10.1109/CSF.2008.7

    work page doi:10.1109/csf.2008.7 2008

  9. [10]

    Thibault Dardinier and Peter Müller. 2024. Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (Extended Version).Proc. ACM Program. Lang.8, PLDI (June 2024), 1485–1509. arXiv:2301.10037 [cs] doi:10.1145/3656437

    work page doi:10.1145/3656437 2024

  10. [11]

    G de Bruijn

    N. G de Bruijn. 1972. Lambda Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem.Indagationes Mathematicae (Proceedings)75, 5 (Jan. 1972), 381–392. doi:10.1016/1385-7258(72)90034-0

    work page doi:10.1016/1385-7258(72)90034-0 1972

  11. [12]

    Edsko de Vries and Vasileios Koutavas. 2011. Reverse Hoare Logic. InSoftware Engineering and Formal Methods, Gilles Barthe, Alberto Pardo, and Gerardo Schneider (Eds.). Springer, Berlin, Heidelberg, 155–171. doi:10.1007/978-3-642- 24690-6_12

    work page doi:10.1007/978-3-642- 2011

  12. [13]

    Zhang, and Benjamin Delaware

    Robert Dickerson, Qianchuan Ye, Michael K. Zhang, and Benjamin Delaware. 2022. RHLE: Modular Deductive Verification of Relational $$\forall \exists $$Properties. InProgramming Languages and Systems, Ilya Sergey (Ed.). Springer Nature Switzerland, Cham, 67–87. doi:10.1007/978-3-031-21037-2_4

    work page doi:10.1007/978-3-031-21037-2_4 2022

  13. [14]

    Emanuele D’Osualdo, Azadeh Farzan, and Derek Dreyer. 2022. Proving Hypersafety Compositionally.Proc. ACM Program. Lang.6, OOPSLA2 (Oct. 2022), 135:289–135:314. doi:10.1145/3563298

    work page doi:10.1145/3563298 2022

  14. [15]

    Marco Eilers, Thibault Dardinier, and Peter Müller. 2023. CommCSL: Proving Information Flow Security for Concurrent Programs Using Abstract Commutativity.Proc. ACM Program. Lang.7, PLDI (June 2023), 175:1682–175:1707. doi:10. 1145/3591289

    2023

  15. [16]

    Gidon Ernst and Toby Murray. 2019. SecCSL: Security Concurrent Separation Logic. InComputer Aided Verification, Isil Dillig and Serdar Tasiran (Eds.). Vol. 11562. Springer International Publishing, Cham, 208–230. doi:10.1007/978-3- 030-25543-5_13

    work page doi:10.1007/978-3- 2019

  16. [17]

    Robert W. Floyd. 1967. Assigning Meanings to Programs.Proceedings of Symposium in Applied Mathematics(1967), 19–32

    1967

  17. [18]

    Dan Frumin, Robbert Krebbers, and Lars Birkedal. 2018. ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency. InProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS ’18). Association for Computing Machinery, New York, NY, USA, 442–451. doi:10.1145/3209108.3209174

    work page doi:10.1145/3209108.3209174 2018

  18. [19]

    Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, and Derek Dreyer. 2022. Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations.Proc. ACM Program. Lang.6, POPL (Jan. 2022), 28:1–28:31. doi:10.1145/3498689 250:24 Trayan Gospodinov, Peter Müller, and Thibault Dardinier

    work page doi:10.1145/3498689 2022

  19. [20]

    Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens, Saman Amarasinghe, and Ilya Sergey. 2024. Mechanised Hypersafety Proofs about Structured Data.Proc. ACM Program. Lang.8, PLDI (June 2024), 173:647–173:670. doi:10.1145/3656403

    work page doi:10.1145/3656403 2024

  20. [21]

    J. A. Goguen and J. Meseguer. 1982. Security Policies and Security Models. In1982 IEEE Symposium on Security and Privacy. 11–11. doi:10.1109/SP.1982.10014

    work page doi:10.1109/sp.1982.10014 1982

  21. [22]

    Trayan Gospodinov, Peter Müller, and Thibault Dardinier. 2026. Hyper Separation Logic (artifact). Zenodo. doi:10. 5281/zenodo.19091148

    2026

  22. [23]

    C. A. R. Hoare. 1969. An Axiomatic Basis for Computer Programming.Commun. ACM12, 10 (Oct. 1969), 576–580. doi:10.1145/363235.363259

    work page doi:10.1145/363235.363259 1969

  23. [24]

    Petar Maksimović, Caroline Cronjäger, Andreas Lööw, Julian Sutherland, and Philippa Gardner. 2023. Exact Separation Logic: Towards Bridging the Gap Between Verification and Bug-Finding. In37th European Conference on Object- Oriented Programming (ECOOP 2023) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 263), Karim Ali and Guido Salvanes...

    work page doi:10.4230/lipics.ecoop.2023.19 2023

  24. [25]

    Daryl McCullough. 1987. Specifications for Multi-Level Security and a Hook-Up. In1987 IEEE Symposium on Security and Privacy. 161–161. doi:10.1109/SP.1987.10009

    work page doi:10.1109/sp.1987.10009 1987

  25. [26]

    McCullough

    D. McCullough. 1988. Noninterference and the Composability of Security Properties. InProceedings. 1988 IEEE Symposium on Security and Privacy. 177–186. doi:10.1109/SECPRI.1988.8110

    work page doi:10.1109/secpri.1988.8110 1988

  26. [27]

    Possibilistic

    J. McLean. 1996. A General Theory of Composition for a Class of "Possibilistic" Properties.IEEE Transactions on Software Engineering22, 1 (Jan. 1996), 53–67. doi:10.1109/32.481534

    work page doi:10.1109/32.481534 1996

  27. [28]

    Toby Murray. 2020. An Under-Approximate Relational Logic: Heralding Logics of Insecurity, Incorrect Implementation & More. arXiv:2003.04791 [cs] doi:10.48550/arXiv.2003.04791

    work page doi:10.48550/arxiv.2003.04791 2020

  28. [29]

    Toby Murray, Pengbo Yan, and Gidon Ernst. 2023. Compositional Vulnerability Detection with Insecurity Separation Logic. InFormal Methods and Software Engineering, Yi Li and Sofiène Tahar (Eds.). Springer Nature, Singapore, 65–82. doi:10.1007/978-981-99-7584-6_5

    work page doi:10.1007/978-981-99-7584-6_5 2023

  29. [30]

    Paulson, and Markus Wenzel

    Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002.Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, Vol. 2283. Springer. doi:10.1007/3-540-45949-9

    work page doi:10.1007/3-540-45949-9 2002

  30. [31]

    Peter W. O’Hearn. 2019. Incorrectness Logic.Proc. ACM Program. Lang.4, POPL (Dec. 2019), 10:1–10:32. doi:10.1145/ 3371078

    2019

  31. [32]

    Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter O’Hearn, and Jules Villard. 2020. Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic. InComputer Aided Verification, Shuvendu K. Lahiri and Chao Wang (Eds.). Springer International Publishing, Cham, 225–252. doi:10.1007/978-3-030-53291-8_14

    work page doi:10.1007/978-3-030-53291-8_14 2020

  32. [33]

    Azalea Raad, Josh Berdine, Derek Dreyer, and Peter W. O’Hearn. 2022. Concurrent Incorrectness Separation Logic. Proc. ACM Program. Lang.6, POPL (Jan. 2022), 34:1–34:29. doi:10.1145/3498695

    work page doi:10.1145/3498695 2022

  33. [34]

    Reynolds

    J.C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. InProceedings 17th Annual IEEE Symposium on Logic in Computer Science. 55–74. doi:10.1109/LICS.2002.1029817

    work page doi:10.1109/lics.2002.1029817 2002

  34. [35]

    Marcelo Sousa and Isil Dillig. 2016. Cartesian Hoare Logic for Verifying K-Safety Properties. InProceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’16). Association for Computing Machinery, New York, NY, USA, 57–69. doi:10.1145/2908080.2908092

    work page doi:10.1145/2908080.2908092 2016

  35. [36]

    Hongseok Yang. 2007. Relational Separation Logic.Theoretical Computer Science375, 1 (May 2007), 308–334. doi:10. 1016/j.tcs.2006.12.036

    2007

  36. [37]

    Noam Zilberstein, Derek Dreyer, and Alexandra Silva. 2023. Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning.Proc. ACM Program. Lang.7, OOPSLA1 (April 2023), 93:522–93:550. doi:10.1145/3586045

    work page doi:10.1145/3586045 2023

  37. [38]

    De Bruijn store

    Noam Zilberstein, Angelina Saliling, and Alexandra Silva. 2024. Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects.Proc. ACM Program. Lang.8, OOPSLA1 (April 2024), 104:276–104:304. doi:10.1145/3649821 Hyper Separation Logic 250:25 ⟨𝑥:=𝑒,⟨𝑠, ℎ⟩⟩ → ⟨skip,⟨𝑠[𝑥↦→𝑒(𝑠)], ℎ⟩⟩⟨𝑥:=nonDet(),⟨𝑠, ℎ⟩⟩ → ⟨skip,⟨𝑠[𝑥↦→𝑣...

    work page doi:10.1145/3649821 2024