pith. sign in

arxiv: 2601.20370 · v2 · submitted 2026-01-28 · 💻 cs.LO · cs.PL

A Program Logic for Abstract (Hyper)Properties

Paolo Baldan , Roberto Bruni , Francesco Ranzato , Diletta Rigo This is my paper

Pith reviewed 2026-05-16 10:20 UTC · model grok-4.3

classification 💻 cs.LO cs.PL
keywords program logicHoare logicabstract interpretationhyperpropertiessoundnessrelative completenessmonoidal operatornondeterminism
0
0 comments X

The pith

APPL is a sound Hoare-style logic for abstract program properties and hyperproperties that becomes relatively complete when the abstract domain is complete for its monoidal operator.

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

The paper presents APPL as a single proof system that recovers standard Hoare logic, incorrectness logic, and multiple hyperproperty variants as special cases. It builds a semantic model in which commands act on lattices and nondeterministic choice is interpreted by a monoidal operator that need not be idempotent or coincide with the lattice join; this choice lets the same logic cover collecting semantics, abstract semantics, and hypersemantics. The resulting system is sound in general and relatively complete whenever the property language is expressive enough. When properties are restricted to an abstract domain, the logic yields a sound deductive system based on best correct approximations, with relative completeness restored precisely when the domain is complete for the monoidal operator in the sense of abstract interpretation.

Core claim

APPL supplies a unifying Hoare-style logic whose semantics first define command meanings on a lattice basis and then extend them additively; nondeterministic choice is handled by a monoidal operator that can represent collecting, abstract, or hyper semantics. The proof system is sound for any sufficiently expressive property language and is relatively complete for that language; when the language is replaced by an abstract domain, the system remains sound via best correct approximations and recovers relative completeness exactly when the domain is complete for the monoidal operator.

What carries the argument

The monoidal operator interpreting nondeterministic choice, which need not be idempotent or equal to the lattice join and thereby enables the uniform treatment of collecting, abstract, and hypersemantics.

If this is right

  • Standard Hoare logic, incorrectness logic, and existing hyper Hoare logics are recovered as instances of APPL.
  • Abstract program properties can be reasoned about deductively using best correct approximations without leaving the logic.
  • Hyperproperties are handled uniformly inside the same proof system rather than by separate formalisms.
  • Relative completeness holds for any property language expressive enough to denote the required predicates.

Where Pith is reading between the lines

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

  • The same monoidal-operator approach could be applied to develop deductive systems for other forms of abstraction such as probabilistic or quantum semantics.
  • Completeness of the abstract domain for the operator becomes a practical design criterion when building new abstract interpreters that support proof automation.
  • The framework suggests a route to combine under- and over-approximations inside one logic by choosing different monoidal operators for different fragments.

Load-bearing premise

The abstract domain must be complete for the chosen monoidal operator; if completeness fails, relative completeness with respect to the abstract semantics is lost.

What would settle it

An abstract domain that is not complete for the monoidal operator yet still admits relative completeness of the APPL system for the corresponding abstract semantics would falsify the necessity of the completeness condition.

Figures

Figures reproduced from arXiv: 2601.20370 by Diletta Rigo, Francesco Ranzato, Paolo Baldan, Roberto Bruni.

Figure 1
Figure 1. Figure 1: The program logic APPL over the interpretation monoid [PITH_FULL_IMAGE:figures/full_fig_p010_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Derivation for Example 3.7 3.2.3 Incorrectness Logic. As discussed in § 2.4.3, incorrectness logic can be recovered by relying on the interpretation monoid (℘(Σ), ⊇, ∪, ℘(Σ)). In this setting, the full semantics coincides with the basis one, i.e., JrK = LrM. Consequently, the additive extension is trivial, rendering the (join) rule redundant in the proof system. While relative completeness already guarante… view at source ↗
Figure 3
Figure 3. Figure 3: Derivation for Example 3.8 (join) {{𝑃0} , {𝑃2}} dense (choice) ⊢ ⟨{𝑃0}⟩ 1 ⟨{𝑃0}⟩ ⊢ ⟨{𝑃0}⟩ 𝑥 := 𝑥 + 1 ⟨{𝑃1}⟩ ⊢ ⟨{𝑃0}⟩ 1 + (𝑥 := 𝑥 + 1) ⟨{𝑃0 ⊕ 𝑃1}⟩ (choice) ⊢ ⟨{𝑃2}⟩ 1 ⟨{𝑃2}⟩ ⊢ ⟨{𝑃2}⟩ 𝑥 := 𝑥 + 1 ⟨{𝑃3}⟩ ⊢ ⟨{𝑃2}⟩ 1 + (𝑥 := 𝑥 + 1) ⟨{𝑃2 ⊕ 𝑃3}⟩ {𝑃0 ⊕ 𝑃1} ∪ {𝑃2 ⊕ 𝑃3} ⊆ {𝑃0 ⊕ 𝑃1, 𝑃2 ⊕ 𝑃3} ⊢ ⟨{𝑃0, 𝑃2}⟩ 1 + (𝑥 := 𝑥 + 1) ⟨{𝑃0 ⊕ 𝑃1, 𝑃2 ⊕ 𝑃3}⟩ [PITH_FULL_IMAGE:figures/full_fig_p014_3.png] view at source ↗
Figure 5
Figure 5. Figure 5: The abstract program logic APPL𝐴: some key rules, where JeK 𝐴𝑎 abbreviates Ã𝐴 {LeM 𝐴𝑏 ∈ 𝐴 | 𝑏 ∈ 𝛼 (B), 𝛼 (𝑏) ⊑𝐴 𝑎}. Indeed, the premise of the abstract (join) rule requires the family {𝑎𝑖 | 𝑖 ∈ 𝐼 } to be dense in 𝐴. By Lemma 4.1 (2), density in 𝐴 implies density of {𝛾 (𝑎𝑖)} in 𝐷, but the reverse is not generally true. Thus, the abstract requirement is stronger (less permissive) than the con￾crete one. Howe… view at source ↗
Figure 6
Figure 6. Figure 6: A derivation in ℘(Int) ↓ , with 𝑇2 ≜ {[2𝑛, 2𝑛]}𝑛∈N and 𝑇 + 2 ≜ {[2𝑛, 2𝑛]}𝑛∈N\{0} 5.2 Pointwise Abstraction Given a Galois insertion 𝐶 −−−→−→ ←−−−− 𝛼 𝛾 𝐴, we consider the abstrac￾tion for hyperproperties that applies the underlying abstraction 𝛼 pointwise to the elements of a hyperproperty. Formally, we define the Galois insertion ℘(𝐶) −−−−→−→ ←−−−−− 𝛼𝑝 𝛾𝑝 ℘(𝐴), where, for 𝑋 ∈ ℘(𝐶), we let 𝛼𝑝 (𝑋) ≜ {𝛼 (𝑐) |… view at source ↗
Figure 7
Figure 7. Figure 7: Derivation for Example 5.6, where 𝑎0 ≜ [{1, 999}, [1, 999]]. Interestingly, this framework yields a logic for certifying that a specific abstract evaluation corresponds to the BCA—intended as the abstraction of the concrete semantics—a problem recently tack￾led in [16]. More precisely, the logic is always sound and complete when the lattice 𝐶 is completely distributive (hence, in particular, when (𝐶, ≤) = … view at source ↗
Figure 8
Figure 8. Figure 8: Derivation of ⊢ ⟨[{−1, 0, 1}, [−1, 1]]⟩ p ⟨[∅, ∅]⟩ tracking 𝑥 < 0 ⇒ 𝑥 ∈ [−1, −1] and 𝑥 ≥ 0 ⇒ 𝑥 ∈ [1, 1]. A simi￾lar effect is achieved via our (join) rule, letting the analysis retain branch-sensitive information. As a concrete example, consider the command v ≜ [PITH_FULL_IMAGE:figures/full_fig_p020_8.png] view at source ↗
read the original abstract

We introduce APPL (Abstract Program Property Logic), a unifying Hoare-style logic that subsumes standard Hoare logic, incorrectness logic, and several variants of Hyper Hoare logic. APPL provides a principled foundation for abstract program logics parameterised by an abstract domain, encompassing both existing and novel abstractions of properties and hyperproperties. The logic is grounded in a semantic framework where the meaning of commands is first defined on a lattice basis and then extended to the full lattice via additivity. Crucially, nondeterministic choice is interpreted by a monoidal operator that need not be idempotent nor coincide with the lattice join. This flexibility allows the framework to capture collecting semantics, various classes of abstract semantics, and hypersemantics. The APPL proof system is sound, and it is relatively complete whenever the property language is sufficiently expressive. When the property language is restricted to an abstract domain, the result is a sound abstract deduction system based on best correct approximations. Relative completeness with respect to a corresponding abstract semantics is recovered provided the abstract domain is complete, in the sense of abstract interpretation, for the monoidal operator.

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

2 major / 2 minor

Summary. The paper introduces APPL, a Hoare-style program logic parameterized by an abstract domain and a monoidal operator. It unifies standard Hoare logic, incorrectness logic, and variants of Hyper Hoare logic by defining command semantics first on a lattice basis and extending via additivity, with nondeterministic choice interpreted by a general monoidal operator (not necessarily idempotent or equal to lattice join). The central claims are that the APPL proof system is sound in general and relatively complete when the property language is sufficiently expressive; when restricted to an abstract domain it yields a sound abstract deduction system based on best correct approximations, with relative completeness recovered if the abstract domain is complete (in the abstract-interpretation sense) for the monoidal operator.

Significance. If the soundness and conditional relative-completeness results hold, the framework supplies a principled, unifying foundation for abstract program logics that can capture both ordinary properties and hyperproperties. The explicit separation of lattice-based collecting semantics from a flexible monoidal operator for choice is a genuine technical contribution that goes beyond standard abstract-interpretation treatments and directly supports the unification claim.

major comments (2)
  1. [Proofs of Theorems 1 and 2 (or equivalent)] The soundness and relative-completeness theorems are stated in the abstract and presumably proved in the main body, yet the provided description contains no proof sketches or key lemmas. Without these derivations it is impossible to verify that the lattice extension via additivity preserves the required properties of the monoidal operator or that the best-correct-approximation construction interacts correctly with the proof rules.
  2. [Section on abstract semantics and completeness] The relative-completeness claim for abstract domains is conditioned on the abstract domain being complete for the monoidal operator. The manuscript should supply either a concrete counter-example showing loss of completeness when this condition fails, or an explicit statement of the additional proof obligations this completeness assumption discharges in the abstract semantics.
minor comments (2)
  1. Notation for the monoidal operator, lattice operations, and abstract-domain concretization should be introduced uniformly in a single preliminary section rather than piecemeal.
  2. The abstract claims the logic 'subsumes' several existing systems; a short table or paragraph explicitly mapping APPL rules to the corresponding rules of Hoare logic, incorrectness logic, and one hyperproperty logic would strengthen the unification claim.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the positive evaluation of the paper's significance and for the constructive comments. We address each major comment below and will revise the manuscript to incorporate the requested clarifications and examples.

read point-by-point responses

  1. Referee: [Proofs of Theorems 1 and 2 (or equivalent)] The soundness and relative-completeness theorems are stated in the abstract and presumably proved in the main body, yet the provided description contains no proof sketches or key lemmas. Without these derivations it is impossible to verify that the lattice extension via additivity preserves the required properties of the monoidal operator or that the best-correct-approximation construction interacts correctly with the proof rules.

    Authors: The full manuscript contains the complete proofs of Theorem 1 (soundness) in Section 4 and Theorem 2 (relative completeness) in Section 5, supported by Lemmas 4.1--4.3 establishing preservation of monoidal properties under additive extension and Lemma 5.2 on the interaction between best-correct approximations and the proof rules. These derivations confirm that additivity preserves the required algebraic properties by construction. To address accessibility, we will insert concise proof sketches immediately after each theorem statement in the revised main text. revision: yes

  2. Referee: [Section on abstract semantics and completeness] The relative-completeness claim for abstract domains is conditioned on the abstract domain being complete for the monoidal operator. The manuscript should supply either a concrete counter-example showing loss of completeness when this condition fails, or an explicit statement of the additional proof obligations this completeness assumption discharges in the abstract semantics.

    Authors: We agree that the completeness assumption benefits from concrete illustration. In the revised manuscript we will add a new subsection in Section 6 containing a concrete counter-example of an abstract domain that is not complete for the monoidal operator, together with the resulting loss of relative completeness in the abstract deduction system. This will make the necessity of the assumption explicit while leaving the main theorems unchanged. revision: yes

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper grounds APPL in an external lattice-based collecting semantics extended by additivity, with nondeterministic choice via a general monoidal operator. Soundness follows directly from this semantics, and relative completeness is conditioned explicitly on the property language being sufficiently expressive or the abstract domain being complete for the monoidal operator. No equation or derivation reduces the claimed results back to a fitted parameter, self-definition, or self-citation chain; the setup unifies prior logics without internal collapse to its own inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 3 axioms · 0 invented entities

The framework rests on standard lattice theory and abstract-interpretation completeness notions; no new free parameters or invented entities are introduced beyond the monoidal operator chosen by the user of the logic.

axioms (3)
  • standard math The semantic domain forms a lattice with additive extension from a basis
    Invoked to define command meanings before extending to the full lattice
  • domain assumption Nondeterministic choice is interpreted by a monoidal operator that need not be idempotent or equal to lattice join
    Central flexibility that allows capturing collecting, abstract, and hypersemantics
  • domain assumption Abstract domain completeness for the monoidal operator
    Required to recover relative completeness in the abstract case

pith-pipeline@v0.9.0 · 5496 in / 1503 out tokens · 33723 ms · 2026-05-16T10:20:41.541500+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

41 extracted references · 41 canonical work pages

  1. [1]

    Flavio Ascari, Roberto Bruni, and Roberta Gori. 2025. Broadening the applicability of local completeness analysis with intensional and extensional guarantees. Theoretical Computer Science1054 (2025), 115452. doi:10.1016/J.TCS.2025.115452

    work page doi:10.1016/j.tcs.2025.115452 2025

  2. [2]

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

    work page doi:10.1145/3720486 2025

  3. [3]

    Flavio Ascari, Roberto Bruni, Roberta Gori, and Azalea Raad. 2026. U-Turn: Enhancing Incorrectness Analysis by Reversing Direction.Proc. ACM Program. Lang.10, POPL, Article 46 (Jan. 2026), 27 pages. doi:10.1145/3776688

    work page doi:10.1145/3776688 2026

  4. [4]

    Naumann, Julien Signoles, Éric Totel, and Frédéric Tronel

    Mounir Assaf, David A. Naumann, Julien Signoles, Éric Totel, and Frédéric Tronel. 2017. Hypercollecting semantics and its application to static analysis of information flow. InProceedings of POPL 2017. ACM, 874–887. doi:10.1145/ 3009837.3009889

    work page arXiv 2017

  5. [5]

    Roberto Bruni, Roberto Giacobazzi, Roberta Gori, and Francesco Ranzato. 2021. A Logic for Locally Complete Abstract Interpretations. InProceedings of LICS 2021, 36th Annual ACM/IEEE Symposium on Logic in Computer Science. IEEE, 1–13. doi:10.1109/LICS52264.2021.9470608 Distinguished paper

    work page doi:10.1109/lics52264.2021.9470608 2021

  6. [6]

    Roberto Bruni, Roberto Giacobazzi, Roberta Gori, and Francesco Ranzato. 2023. A Correctness and Incorrectness Program Logic.J. ACM70, 2 (2023), 15:1–15:45. doi:10.1145/3582267

    work page doi:10.1145/3582267 2023

  7. [7]

    Marco Campion, Mila Dalla Preda, Roberto Giacobazzi, and Caterina Urban. 2026. A Logic for the Imprecision of Abstract Interpretations.Proc. ACM Program. Lang.10, POPL, Article 65 (2026), 29 pages. doi:10.1145/3776707

    work page doi:10.1145/3776707 2026

  8. [8]

    2021.Principles of Abstract Interpretation

    Patrick Cousot. 2021.Principles of Abstract Interpretation. MIT Press

    work page 2021

  9. [9]

    Patrick Cousot. 2024. Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation.Proc. ACM Program. Lang.8, POPL (2024), 175–208. doi:10.1145/3632849 20 A Program Logic for Abstract (Hyper)Properties

    work page doi:10.1145/3632849 2024

  10. [10]

    Abstract interpretation: A un ified lattice model for static analysis of programs by construction or app roximation of fixpoints,

    P. Cousot and R. Cousot. 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. InConference Record of the 4th ACM Symposium on Principles of Programming Languages(POPL ’77). ACM Press, 238–252. doi:10.1145/512950.512973

    work page doi:10.1145/512950.512973 1977

  11. [11]

    Patrick Cousot, Radhia Cousot, Francesco Logozzo, and Michael Barnett. 2012. An abstract interpretation framework for refactoring with application to extract methods with contracts. InProceedings of OOPSLA. ACM, 213–232. doi:10.1145/ 2384616.2384633

    work page arXiv 2012

  12. [12]

    Patrick Cousot and Jeffery Wang. 2025. Calculational Design of Hyperlogics by Abstract Interpretation.Proceedings of the ACM on Programming Languages9, POPL (2025), 446–478. doi:10.1145/3704852

    work page doi:10.1145/3704852 2025

  13. [13]

    Thibault Dardinier and Peter Müller. 2024. Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties.Proceedings of the ACM on Programming Languages8, PLDI (2024), 1485–1509. doi:10.1145/3656437

    work page doi:10.1145/3656437 2024

  14. [14]

    Roberto Giacobazzi and Isabella Mastroeni. 2004. Abstract non-interference: parameterizing non-interference by abstract interpretation. InProceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16, 2004. ACM, 186–197. doi:10.1145/964001. 964017

    work page doi:10.1145/964001 2004

  15. [15]

    Roberto Giacobazzi and Isabella Mastroeni. 2010. A Proof System for Abstract Non-interference.J. Log. Comput.20, 2 (2010), 449–479. doi:10.1093/LOGCOM/ EXP053

    work page doi:10.1093/logcom/ 2010

  16. [16]

    Roberto Giacobazzi and Francesco Ranzato. 2025. The Best of Abstract Interpreta- tions.Proc. ACM Program. Lang.9, POPL (2025), 1355–1385. doi:10.1145/3704882

    work page doi:10.1145/3704882 2025

  17. [17]

    Roberto Giacobazzi, Francesco Ranzato, and Francesca Scozzari. 2000. Making abstract interpretations complete.J. ACM47, 2 (2000), 361–416. doi:10.1145/ 333979.333989

    work page arXiv 2000

  18. [18]

    Maria Handjieva and Stanislav Tzolovski. 1998. Refining Static Analyses by Trace-Based Partitioning Using Control Flow. InProceedings 5th International Static Analysis Symposium, SAS’98 (Lecture Notes in Computer Science, Vol. 1503). Springer, 200–214. doi:10.1007/3-540-49727-7_12

    work page doi:10.1007/3-540-49727-7_12 1998

  19. [19]

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

    work page doi:10.1145/363235.363259 1969

  20. [20]

    Georg Karner. 2004. Continuous monoids and semirings.Theoretical Computer Science318, 3 (2004), 355–372. doi:10.1016/j.tcs.2004.01.020

    work page doi:10.1016/j.tcs.2004.01.020 2004

  21. [21]

    Dexter Kozen. 1997. Kleene algebra with tests.ACM Trans. Program. Lang. Syst. 19, 3 (May 1997), 427–443. doi:10.1145/256167.256195

    work page doi:10.1145/256167.256195 1997

  22. [22]

    Daniel Krob. 1987. Monoides et semi-anneaux complets.Semigroup Forum36, 1 (1987), 323–339. doi:10.1007/BF02575025

    work page doi:10.1007/bf02575025 1987

  23. [23]

    Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, and Peter W. O’Hearn. 2022. Finding real bugs in big programs with incorrectness logic.Proc. ACM Program. Lang.6, OOPSLA1 (2022), 1–27. doi:10.1145/3527325

    work page doi:10.1145/3527325 2022

  24. [24]

    Isabella Mastroeni and Michele Pasqua. 2017. Hyperhierarchy of Semantics: A Formal Framework for Hyperproperties Verification. InProceedings of SAS 2017 (LNCS, Vol. 10422). Springer, 232–252. doi:10.1007/978-3-319-66706-5_12

    work page doi:10.1007/978-3-319-66706-5_12 2017

  25. [25]

    Isabella Mastroeni and Michele Pasqua. 2018. Verifying Bounded Subset-Closed Hyperproperties. InProceeding of SAS 2018 (LNCS, Vol. 11002). Springer, 263–283. doi:10.1007/978-3-319-99725-4_17

    work page doi:10.1007/978-3-319-99725-4_17 2018

  26. [26]

    Isabella Mastroeni and Michele Pasqua. 2019. Statically analyzing information flows: an abstract interpretation-based hyperanalysis for non-interference. In Proceedings of the 34th ACM/SIGAPP Symposium on Applied Computing, SAC 2019. ACM, 2215–2223. doi:10.1145/3297280.3297498

    work page doi:10.1145/3297280.3297498 2019

  27. [27]

    A. Miné. 2017. Tutorial on static inference of numeric invariants by abstract interpretation.Foundations and Trends in Programming Languages4, 3-4 (2017), 120–372. doi:10.1561/2500000034

    work page doi:10.1561/2500000034 2017

  28. [28]

    Peter W. O’Hearn. 2019. Incorrectness logic.Proc. ACM Program. Lang.4, POPL, Article 10 (dec 2019), 32 pages. doi:10.1145/3371078

    work page doi:10.1145/3371078 2019

  29. [29]

    O’Hearn, and Jules Villard

    Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter W. O’Hearn, and Jules Villard. 2020. Local Reasoning About the Presence of Bugs: Incorrect- ness Separation Logic. InProceedings of CA V 2020 (Lecture Notes in Computer Science, Vol. 12225). Springer, 225–252. doi:10.1007/978-3-030-53291-8_14

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

  30. [30]

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

    work page doi:10.1145/3498695 2022

  31. [31]

    Azalea Raad, Julien Vanegue, and Peter W. O’Hearn. 2024. Non-termination Proving at Scale.Proc. ACM Program. Lang.8, OOPSLA2 (2024), 246–274. doi:10. 1145/3689720

    work page 2024

  32. [32]

    Xavier Rival and Laurent Mauborgne. 2007. The trace partitioning abstract domain.ACM Trans. Program. Lang. Syst.29, 5 (2007), 26. https://doi.org/10. 1145/1275497.1275501

    work page arXiv 2007

  33. [33]

    Lena Verscht and Benjamin Lucien Kaminski. 2025. A Taxonomy of Hoare- Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests.Proc. ACM Program. Lang.9, POPL (2025), 1782–

    work page 2025

  34. [34]

    Lena Verscht, Anrán Wáng, and Benjamin Lucien Kaminski. 2025. Partial In- correctness Logic.CoRRabs/2502.14626 (2025). arXiv:2502.14626 doi:10.48550/ ARXIV.2502.14626

    work page arXiv 2025

  35. [35]

    Linpeng Zhang and Benjamin Lucien Kaminski. 2022. Quantitative strongest post: a calculus for reasoning about the flow of quantitative information.Proc. ACM Program. Lang.6, OOPSLA1 (2022), 1–29. doi:10.1145/3527331

    work page doi:10.1145/3527331 2022

  36. [36]

    Linpeng Zhang, Noam Zilberstein, Benjamin Lucien Kaminski, and Alexandra Silva. 2024. Quantitative Weakest Hyper Pre: Unifying Correctness and Incor- rectness Hyperproperties via Predicate Transformers.Proc. ACM Program. Lang. 8, OOPSLA2 (2024), 817–845. doi:10.1145/3689740

    work page doi:10.1145/3689740 2024

  37. [37]

    Noam Zilberstein. 2025. Outcome Logic: A Unified Approach to the Metatheory of Program Logics with Branching Effects.ACM Trans. Program. Lang. Syst.47, 3, Article 14 (Sept. 2025), 71 pages. doi:10.1145/3743131

    work page doi:10.1145/3743131 2025

  38. [38]

    Noam Zilberstein, Derek Dreyer, and Alexandra Silva. 2023. Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning.Proceedings of the ACM on Programming Languages7, OOPSLA1 (2023), 522–550. doi:10. 1145/3586045

    work page 2023

  39. [39]

    Noam Zilberstein, Dexter Kozen, Alexandra Silva, and Joseph Tassarotti. 2025. A Demonic Outcome Logic for Randomized Nondeterminism.Proc. ACM Program. Lang.9, POPL (2025), 539–568. doi:10.1145/3704855

    work page doi:10.1145/3704855 2025

  40. [40]

    Noam Zilberstein, Angelina Saliling, and Alexandra Silva. 2024. Outcome Sep- aration Logic: Local Reasoning for Correctness and Incorrectness with Com- putational Effects.Proc. ACM Program. Lang.8, OOPSLA1 (2024), 276–304. doi:10.1145/3649821

    work page doi:10.1145/3649821 2024

  41. [41]

    Noam Zilberstein, Alexandra Silva, and Joseph Tassarotti. 2026. Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants.Proc. ACM Program. Lang.10, POPL, Article 9 (2026), 30 pages. doi:10.1145/3776651 21

    work page doi:10.1145/3776651 2026