Pith. sign in

REVIEW 3 major objections 4 minor 87 references

Calculational Design of Hyperlogics by Abstract Interpretation

T0 review · 3 major / 4 minor · reviewed 2026-08-12 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read One parameterized algebraic abstract interpreter yields sound and complete calculi for execution and hyperproperties, and abstractions of the latter yield simplified proof rules for ∀∃, ∀∀, and ∃∀ hyperproperties.

desk verdict A genuinely ambitious framework for deriving hyperlogics by abstract interpretation, but the headline invalidation of Assaf et al. is exactly where I'd want the appendix checked, and the manuscript has an unfinished TO DO. read the letter →

arxiv 2411.11113 v1 pith:DL67H4B2 submitted 2024-11-17 cs.LO

Patrick Cousot , Jeffery Wang This is my paper · ORCID
classification cs.LO
keywords abstractinterpretationhyperpropertieshyperlogicscalculationaldesignfixpointsemanticssoundnessandcompletenessnonterminationincorrectnesslogic
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper tries to establish that one generic algebraic abstract interpreter, parameterized only by an abstract domain of finite and infinite computations, can serve as the common engine for deriving sound and complete proof calculi for ordinary execution properties (sets of traces) and for semantic hyperproperties (sets of sets of traces). This matters because hyperproperties—like noninterference—relate multiple executions of a program, and existing hyperlogics are either tied to a fixed semantics or incomplete. The paper shows that abstracting the semantic properties themselves, rather than the program semantics, yields simplified proof rules that are still sound and complete for important classes, including forall-exists, forall-forall, and exists-forall hyperproperties. Along the way it identifies an unsound fixed-point equation in a published hypercollecting semantics and replaces it with a corrected 'weak' version.

What carries the argument

The central mechanism is the algebraic abstract domain D♯ = (D♯+, D♯∞), a pair of chain-complete lattices for finite and infinite computations equipped with an associative sequential composition #♯ that preserves joins or is right upper continuous. The execution transformer is post♯(S)P ≜ P #♯ S, and the semantic transformer is Post♯(S)𝒫 ≜ {post♯(S)P | P ∈ 𝒫}; the structurality of Post is recovered through the singleton fixpoint isomorphism of Proposition 6.3, which lets the conditional and while rules be derived calculationally. The abstractions of Part III then map the semantic-property lattice to simpler lattices on which the proof rules can be stated and proved without describing the program semantics exactly.

What would settle it

Take the infinite-trace instantiation of appendix B, where concatenation fails right lower continuity, and check whether the sound and complete Post calculus of Theorem 6.4 still holds for a loop whose body generates the decreasing suffix chain of counterexample B.1; if the while rule (47) computes a set that misses the greatest lower bound of that chain, then the theorem's hypotheses must be tightened and the genericity claim is falsified for infinite behaviours.

Watch

Extended reading notes

Core claim

The central claim is that the same structural fixpoint abstract interpreter that computes the execution transformer post also computes the semantic transformer Post, provided Post is defined element-wise on singleton preconditions. The paper proves sound and complete calculi (Theorems 5.5, 6.4, 7.5) for execution properties and for semantic properties, and then shows that exact or approximate abstractions of the semantic-property lattice—join, homomorphic, order ideal, frontier, chain limit, and their combinations—preserve the algebraic structure and yield tractable proof rules. It further claims that the hypercollecting semantics of [5] is incomplete and that its fixed-point equation (48) is unsound, invalidating [5, Theorem 1]; the corrected weak hypercollecting semantics of (91) restores soundness, and the new chain-limit and order-ideal rules generalize the while rule of [29, 30].

Load-bearing premise

The load-bearing premise is that sequential composition in the chosen abstract domain is associative, chain-complete, and either preserves joins or is right upper continuous; the infinite-trace instantiation of appendix B violates this continuity, so the generic soundness and completeness theorems do not automatically transfer to every semantics the paper mentions.

Editorial extensions

If this is right

  • Theorem 5.5 gives a sound and complete calculus for execution properties that instantiates to relational, denotational, and trace semantics, with classic correctness and incorrectness logics as particular abstractions.
  • Theorem 6.4 yields the first structural fixpoint sound and complete calculus Post for semantic (hyper) properties; the hypercollecting semantics of [5] is shown incomplete and unsound, and the weak hypercollecting semantics of (91) replaces it.
  • The chain limit, order ideal, and frontier abstractions yield new sound and complete proof rules for ∀∃, ∀∀, and ∃∀ hyperproperties, generalising the while rule of [29, 30].
  • Exact abstractions commute with the transformers, so an instance of the algebraic semantics abstracts to another instance of the same algebraic semantics without loss of precision.
  • Because the upper and lower abstract logics are derived from the same structural Post calculus, both over-approximation (correctness) and under-approximation (incorrectness) proof systems are obtained from the same calculational design.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Because right continuity fails for infinite traces (counterexample B.1), the paper's genericity claims require instance-by-instance verification; a useful next step is to characterise the weakest continuity condition under which Theorems 5.5–7.5 still hold for infinite behaviours.
  • Static analyses built on the earlier hypercollecting semantics may need re-examination for soundness on programs with nested or infinite loops, since the corrected weak semantics (91) is complete only relative to the chain-limit abstraction.
  • The abstraction hierarchy suggests a design recipe for future hyperlogics: pick a semantic-property abstraction first, then derive its proof rule from the generic Post calculus, rather than designing the logic from scratch.
  • The singleton-fixpoint technique should transfer to probabilistic and quantum programs, where the paper notes the algebraic semantics can be instantiated; the immediate test is whether the Post calculus remains sound when composition is not right upper continuous.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper proposes a generic algebraic abstract-interpretation framework for program semantics, parameterized by an abstract domain that can describe finite and infinite computations. On top of this semantics it develops calculational designs of a post transformer for execution properties and a Post transformer for semantic (hyper) properties, together with sound and complete proof systems, stated as Theorems 5.5, 6.4, and 7.5. Part II shows that exact abstractions of the semantics induce abstractions of post, Post, and the logics. Part III introduces a hierarchy of semantic-property abstractions (join, homomorphic, elimination, principal ideal, order ideal, frontier order ideal, chain limit, and combinations) and claims to derive simplified sound and complete proof rules, including algebraic generalizations of forall-exists, forall-forall, and exists-forall hyperproperties. A distinctive, load-bearing claim is that the hypercollecting semantics of Assaf et al. [5] is incomplete and that equation (48) of the present paper 'is unsound, invalidating [5, th. 1]' (Example 6.5).

Significance. If the claims are correct, the paper gives a uniform methodology by which several known hyperlogics and several new ones are obtained as instances of one parameterized algebraic abstract interpreter, and it identifies a subtle defect in a widely used hypercollecting semantics. The visible structural derivations are coherent, and the calculational style makes the design steps transparent. I verified the stress-test concern about Example 6.5 directly: under the paper's own definitions the two sides of the alleged inequality are not equal, because the left-hand side of (48) is the set of individual iterates { post♯(¬B)(post♯(if)^n(P)) | n∈N, P∈𝒫 } while the right-hand side is the set of per-P chain limits { post♯(¬B)(⋃_n post♯(if)^n(P)) | P∈𝒫 }; these sets generally differ. Thus the skeptical equality claim does not land. The trace composition is right upper continuous, and Counterexample B.1 concerns right lower continuity, which is not needed for Theorems 5.5, 6.4, or 7.5, so the stated framework does apply to the trace instantiation for the results actually used.

major comments (3)
  1. [Example 6.5, §20.2] The inequality in (48) is correct, but the further claim that (48) 'is unsound, invalidating [5, th. 1]' is not demonstrated in the supplied text. The visible §20.2 gives an intuitive explanation about 'irrelevant limits of infeasible executions', but the actual proof, and presumably a concrete counterexample, is deferred to Theorem R.6 in the appendix, which is not part of the review copy. Because this is a headline contribution, the full proof or a concrete program and hyperproperty showing the unsoundness of [5, Thm. 1] must be included in the reviewed version, not only referenced.
  2. [Closure abstractions, equations (83)–(86)] The supplied manuscript contains an unfinished 'TO DO' marker in the closure-abstraction part, followed by four incomplete equations (83)–(86) intended to define the upper/lower closure abstractions α↑, α↓, and the transformers Post♯↑ and Post♯↓. These definitions are used in the hierarchy of Part III and in the claimed generalizations of hyperlogics, so an unresolved 'TO DO' in this section is a load-bearing gap that must be completed before the manuscript can be considered final.
  3. [Theorems 6.4 and 7.5] The completeness of the Post calculi is 'completeness by construction', because the while rules require the exact fixpoints of the program semantics, as the paper itself notes in §7.2. This is not a flaw, but the distinction between this trivial completeness of the exact calculi and the substantive completeness of the abstracted Part III rules should be stated more prominently; otherwise the label 'sound and complete' for Theorems 6.4 and 7.5 can be misleading to readers who expect completeness relative to a tractable proof system.
minor comments (4)
  1. [Example 6.5, display (48)] The displayed chain of equalities in (48) is type-ambiguous: reading the second and third lines literally as set comprehensions makes them families of sets rather than a single hyperproperty. The intended reading is presumably a union over n∈N, and the union symbol should be made explicit to avoid confusion.
  2. [Definition 3.2 and Section 3.4] The paper asserts that the framework 'can be instantiated for various operational, denotational, or relational program semantics', but Definition 3.2.D lists several distinct continuity hypotheses. Counterexample B.1 shows right lower continuity fails for infinite traces, and while this is not needed for the main theorems, the paper should provide a short table or remark mapping each named instantiation to the clauses of Definition 3.2.D that it satisfies, so that the applicability claim is precise.
  3. [§20.2, Theorem R.6] The discussion of the weak structural hypercollecting semantics (91) and of the incompleteness of rule (90) is heavily dependent on appendix Theorem R.6 and Lemma R.5, but the review copy does not include those appendix sections. The authors should ensure the full version with all appendix references is the version used for review.
  4. [Section 21] The sound and complete rule for ∃∀-hyperproperties is stated only in the main text, with the development of the conjunctive abstractions and the example relegated to Sections S.1 and S.2 of the appendix. A short example in the main text would greatly improve readability.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the claimed calculi and proof rules are derived by equivalence from explicit semantic definitions, with the exact-semantics completeness limitation openly disclosed.

full rationale

The paper's derivation chain is self-contained in the relevant sense: the generic algebraic semantics (Definition 3.2), the post transformer (18), and the hypercollecting transformer Post (31) are explicit definitions, and the calculi and logics in Theorems 5.5, 6.4, and 7.5 are obtained by calculational equivalence from those definitions rather than by fitting parameters to the target results. The paper explicitly discloses that sound and complete hyperlogics require an exact characterization of the program semantics in the proof (Remark after Theorem 7.5), so the completeness-by-construction of the base Post proof system is an acknowledged design tradeoff, not a concealed circular step. The Part III abstractions are defined independently of the target proof rules, and the relative completeness results (e.g., Theorem 20.2) are stated relative to explicitly chosen abstract semantics. The alleged defect in Example 6.5 does not amount to circularity, and the displayed inequality between (48) and the pointwise Post semantics is genuine: (48) collects the individual finite iterations, while the right-hand side collects the per-input limit as a single element, and applying the union-preserving image Post does not make those two sets equal. Citations to the authors' prior work (bi-inductive semantics, fixpoint theorems, calculational design) are background methodology and are not used to forbid alternatives or to import the paper's conclusions.

Assumptions & free parameters 0 free parameters · 6 assumptions · 0 invented entities

No numbers are fitted to data and no physical or formal entities with independent falsifiable handles are introduced. The framework is parameterized by an abstract domain D-sharp and its primitives, which are treated as axioms rather than fitted parameters. The abstractions studied in Part III are mathematical operators on already-defined semantic domains.

assumptions (6)
  • standard math ZFC set theory with ordinals and transfinite induction
    Section 2.2 invokes Von Neumann ordinals, transfinite induction, and well-ordering ranks for fixpoint iteration in Proposition 2.4 and the fixpoint lemmas.
  • standard math Tarski and constructive fixpoint theorems, including convergence at omega for continuous functions
    Propositions 2.3 and 2.4 and the proofs of lemmas 3.6 through 3.12 rely on [23], [81], and [20, Thm. 15.36] for existence and convergence of least and greatest fixpoints.
  • standard math Galois connection and closure operator theorems
    Galois connections, Galois retractions, and Morgan Ward's closure lattice theorem are used throughout Part II and Sections 15 through 19, with background cited to [34] and [83].
  • domain assumption Aczel correspondence between fixpoint definitions and inductive proof rules
    Invoked in Section 7.2 to convert the structural Post calculus into a Hilbert deductive system. This is a background theorem from [2] and [25] rather than something established in this paper.
  • domain assumption Definition 3.2 well-definedness: D+ is an increasing chain-complete join semilattice, D-infinity is a decreasing chain-complete join lattice, and sequential composition is associative with right upper continuity or join preservation
    Theorems 5.5, 6.4, 7.5, and 7.8 and all generic soundness and completeness results are conditional on this axiom. Trace concatenation fails right lower continuity on infinite traces (counterexample B.1), so each semantic instance must be checked separately.
  • domain assumption Programs are predicates: L-sharp is both the domain of program semantics and the domain of execution properties
    Section 5.1 adopts the Hehner and Kozen identification so post and Post are composition operators. The resulting logics are defined relative to this identification, not relative to an independent assertion language.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Calculational Design of Hyperlogics by Abstract Interpretation." pith.science (2026). https://pith.science/paper/DL67H4B2

@misc{pith2026241111113,
  author       = {Pith},
  title        = {Pith review of: Calculational Design of Hyperlogics by Abstract Interpretation},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/DL67H4B2}},
  note         = {Machine review of arXiv:2411.11113}
}
abstract

We design various logics for proving hyper properties of iterative programs by application of abstract interpretation principles. In part I, we design a generic, structural, fixpoint abstract interpreter parameterized by an algebraic abstract domain describing finite and infinite computations that can be instantiated for various operational, denotational, or relational program semantics. Considering semantics as program properties, we define a post algebraic transformer for execution properties (e.g. sets of traces) and a Post algebraic transformer for semantic (hyper) properties (e.g. sets of sets of traces), we provide corresponding calculuses as instances of the generic abstract interpreter, and we derive under and over approximation hyperlogics. In part II, we define exact and approximate semantic abstractions, and show that they preserve the mathematical structure of the algebraic semantics, the collecting semantics post, the hyper collecting semantics Post, and the hyperlogics. Since proofs by sound and complete hyperlogics require an exact characterization of the program semantics within the proof, we consider in part III abstractions of the (hyper) semantic properties that yield simplified proof rules. These abstractions include the join, the homomorphic, the elimination, the principal ideal, the order ideal, the frontier order ideal, and the chain limit algebraic abstractions, as well as their combinations, that lead to new algebraic generalizations of hyperlogics, including the \forall\exists^\ast$, $\forall\forall^\ast$, and $\exists\forall-^\ast$ hyperlogics,

Figures

Figures reproduced from arXiv: 2411.11113 by the authors.

Figure 2
Figure 2. C abstract logic asing and exte {𝑄 ∣ ∃𝑃 ∈ P esponding logi PiL [PITH_FULL_IMAGE:figures/full_fig_p025_2.png] view at source ↗
Figure 1
Figure 1. The hierarchy of hyperproperties by abstraction. The arrow is interpreted as “more general than” [PITH_FULL_IMAGE:figures/full_fig_p028_1.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

87 extracted references · 42 canonical work pages

  1. [5]

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

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

    arXiv 2017

  2. [1]

    Samson Abramsky. 1991. Domain Theory in Logical Form. Ann. Pure Appl. Log. 51, 1-2 (1991), 1–77. https: //doi.org/10.1016/0168-0072(91)90065-T

    doi:10.1016/0168-0072(91)90065-t 1991

  3. [2]

    Peter Aczel. 1977. An Introduction to Inductive Definitions. In Handbook of Mathematical Logic , John Barwise (Ed.). North–Holland, Amsterdam, Chapter 7, 739–782

    1977

  4. [3]

    Naumann, and Minh Ngo

    Timos Antonopoulos, Eric Koskinen, Ton Chanh Le, Ramana Nagasamudram, David A. Naumann, and Minh Ngo

  5. [4]

    Apt and Gordon D

    Krzysztof R. Apt and Gordon D. Plotkin. 1986. Countable Nondeterminism and Random Assignment. J. ACM 33, 4 (1986), 724–767. https://doi.org/10.1145/6490.6494

    arXiv 1986

  6. [6]

    Raven Beutner. 2024. Automated Software Verification of Hyperliveness. In TACAS (2) (Lecture Notes in Computer Science, Vol. 14571). Springer, 196–216. https://doi.org/10.1007/978-3-031-57249-4_10

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

  7. [7]

    Raven Beutner and Bernd Finkbeiner. 2022. Software Verification of Hyperproperties Beyond k-Safety. In CA V (1) (Lecture Notes in Computer Science, Vol. 13371) . Springer, 341–362. https://doi.org/10.1007/978-3-031-13185-1_17

    doi:10.1007/978-3-031-13185-1_17 2022

  8. [8]

    Raven Beutner and Bernd Finkbeiner. 2023. HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems. Log. Methods Comput. Sci. 19, 2 (2023), 13:1–13:44. https://doi.org/10.46298/LMCS-19(2:13)2023

    doi:10.46298/lmcs-19(2:13)2023 2023

Show all 87 references
  1. [9]

    Raven Beutner, Bernd Finkbeiner, Hadar Frenkel, and Niklas Metzger. 2023. Second-Order Hyperproperties. In CA V (2) (Lecture Notes in Computer Science, Vol. 13965) . Springer, 309–332. https://doi.org/10.1007/978-3-031-37703-7_15

    2023 doi

  2. [10]

    Raven Beutner, Bernd Finkbeiner, Hadar Frenkel, and Niklas Metzger. 2024. Monitoring Second-Order Hyperproperties. In AAMAS. International Foundation for Autonomous Agents and Multiagent Systems / ACM, 180–188. https: //doi.org/10.5555/3635637.3662865

    2024

  3. [11]

    Thomas S. Blyth. 2005. Lattices and Ordered Algebraic Structures . Springer. https://doi.org/10.1007/b139095

    2005 doi

  4. [12]

    Manfred Broy, Martin Wirsing, and Peter Pepper. 1987. On the Algebraic Definition of Programming Languages. ACM Trans. Program. Lang. Syst. 9, 1 (1987), 54–99. https://doi.org/10.1145/9758.10501

    1987

  5. [13]

    Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K

    Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and César Sánchez

  6. [14]

    Clarkson and Fred B

    Michael R. Clarkson and Fred B. Schneider. 2010. Hyperproperties. J. Comput. Secur. 18, 6 (2010), 1157–1210. https://doi.org/10.3233/JCS-2009-0393

    2010 doi

  7. [15]

    Norine Coenen, Bernd Finkbeiner, César Sánchez, and Leander Tentrup. 2019. Verifying Hyperliveness. In CA V (1) (Lecture Notes in Computer Science, Vol. 11561) . Springer, 121–139. https://doi.org/10.1007/978-3-030-25540-4_7

    2019 doi

  8. [16]

    Ellis S. Cohen. 1977. Information Transmission in Computational Systems. In SOSP. ACM, 133–139. https://doi.org/10. 1145/800214.806556

    1977

  9. [17]

    Bruno Courcelle and Maurice Nivat. 1978. The Algebraic Semantics of Recursive Program Schemes. In Mathematical Foundations of Computer Science 1978, Proceedings, 7th Symposium, Zakopane, Poland, September 4-8, 1978 (Lecture Notes in Computer Science, Vol. 64), Józef Winkowski ...

    1978 doi

  10. [18]

    Patrick Cousot. 2002. Constructive Design of a Hierarchy of Semantics of a Transition System by Abstract Interpretation. Theor. Comput. Sci. 277, 1–2 (2002), 47–103. https://doi.org/10.1016/S0304-3975(00)00313-3

    2002 doi

  11. [19]

    Patrick Cousot. 2019. On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics. In LOPSTR (Lecture Notes in Computer Science, Vol. 12042) . Springer, 3–18. https: //doi.org/10.1007/978-3-030-45260-5_1

    2019 doi

  12. [20]

    Patrick Cousot. 2021. Principles of Abstract Interpretation (1 ed.). MIT Press. Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 16. Publication date: January 2025. 16:30 P. Cousot and J. Wang

    2021

  13. [22]

    Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation

    Patrick Cousot. 2024. Full version of “Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation”, Proc. ACM Program. Lang. 8, POPL (2024), 7:1–10:33, https://doi.org/10.1145/3632849. Zenodo (Dec. 2024), 66 pages. https://doi.org/10.528...

    2024 doi

  14. [23]

    Patrick Cousot and Radhia Cousot. 1979. Constructive Versions of Tarski’s Fixed Point Theorems. Pacific J. of Math. 82, 1 (1979), 43–57. https://doi.org/10.2140/pjm.1979.82.43

    1979 doi

  15. [24]

    Patrick Cousot and Radhia Cousot. 1992. Inductive Definitions, Semantics and Abstract Interpretation. In POPL. ACM Press, 83–94. https://doi.org/10.1145/143165.143184

    1992

  16. [25]

    Patrick Cousot and Radhia Cousot. 1995. Compositional and Inductive Semantic Definitions in Fixpoint, Equational, Constraint, Closure-condition, Rule-based and Game-Theoretic Form. In CA V (Lecture Notes in Computer Science, Vol. 939). Springer, 293–308. https://doi.org/10.100...

    1995 doi

  17. [26]

    Patrick Cousot and Radhia Cousot. 2009. Bi-inductive structural semantics. Inf. Comput. 207, 2 (2009), 258–283. https://doi.org/10.1016/J.IC.2008.03.025

    2009 doi

  18. [27]

    Patrick Cousot and Radhia Cousot. 2012. An abstract interpretation framework for termination. In POPL. ACM, 245–258. https://doi.org/10.1145/2103656.2103687

    2012

  19. [28]

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

    2012

  20. [29]

    Thibault Dardinier. 2024. Formalization of Hyper Hoare Logic: A Logic to (Dis-)Prove Program Hyperproperties. Arch. Formal Proofs, 2023. https://www.isa-afp.org/entries/HyperHoareLogic.html

    2024

  21. [30]

    Thibault Dardinier and Peter Müller. 2024. Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties. Proceedings of the ACM on Programming Languages (PACMPL) 8, Issue PLDI, Article No.: 207 (June 2024), 1485–1509. https: //doi.org/10.1145/3656437

    2024 doi

  22. [31]

    Davey and Hilary A

    Brian A. Davey and Hilary A. Priestley. 2002. Introduction to Lattices and Order, Second Edition . Cambridge University Press. https://doi.org/10.1017/CBO9780511809088

    2002 doi

  23. [32]

    Edsko de Vries and Vasileios Koutavas. 2011. Reverse Hoare Logic. In SEFM (Lecture Notes in Computer Science, Vol. 7041). Springer, 155–171. https://doi.org/10.1007/978-3-642-24690-6_12

    2011 doi

  24. [33]

    Jerry den Hartog and Erik P. de Vink. 2002. Verifying Probabilistic Programs Using a Hoare Like Logic. Int. J. Found. Comput. Sci. 13, 3 (2002), 315–340. https://doi.org/10.1142/S012905410200114X

    2002 doi

  25. [34]

    Klaus Denecke, Marcel Erné, and Shelly L. Wismath. 2003. Galois Connections and Applications. Kluwer Academic Publishers. https://doi.org/10.1007/978-1-4020-1898-5

    2003 doi

  26. [35]

    Zhang, and Benjamin Delaware

    Robert Dickerson, Qianchuan Ye, Michael K. Zhang, and Benjamin Delaware. 2022. RHLE: Modular Deductive Verification of Relational ∀ ∃ Properties. In APLAS (Lecture Notes in Computer Science, Vol. 13658) . Springer, 67–87. https://doi.org/10.1007/978-3-031-21037-2_4

    2022 doi

  27. [36]

    Dijkstra

    Edsger W. Dijkstra. 1978. Program Inversion. In Program Construction, International Summer School, July 26 - August 6, 1978, Marktoberdorf, Germany (Lecture Notes in Computer Science, Vol. 69) , Friedrich L. Bauer and Manfred Broy (Eds.). Springer, 54–57. https://doi.org/10.10...

    1978 doi

  28. [37]

    Andrei P. Ershov. 1979. Abstract computability on algebraic structures. In Algorithms in Modern Mathematics and Computer Science (Lecture Notes in Computer Science, Vol. 122) . Springer, 397–420. https://doi.org/10.1007/3-540-11157- 3_38

    1979 doi

  29. [38]

    M. Escardó. 2003. Joins in the frame of nuclei. Applied Categorical Structures 11, 2 (April 2003), 117–124

    2003

  30. [39]

    Yuan Feng and Sanjiang Li. 2023. Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs. Inf. Comput. 294 (2023), 105077. https://doi.org/10.1016/J.IC.2023.105077

    2023

  31. [40]

    Bernd Finkbeiner and Christopher Hahn. 2016. Deciding Hyperproperties. In CONCUR (LIPIcs, Vol. 59) . Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 13:1–13:14. https://doi.org/10.4230/LIPICS.CONCUR.2016.13

    2016 doi

  32. [41]

    Roberto Giacobazzi and Isabella Mastroeni. 2005. Transforming semantics by abstract interpretation. Theor. Comput. Sci. 337, 1-3 (2005), 1–50. https://doi.org/10.1016/J.TCS.2004.12.021

    2005 doi

  33. [42]

    Roberto Giacobazzi and Isabella Mastroeni. 2018. Abstract Non-Interference: A Unifying Framework for Weakening Information-flow. ACM Trans. Priv. Secur. 21, 2 (2018), 9:1–9:31. https://doi.org/10.1145/3175660

    2018 doi

  34. [43]

    Roberto Giacobazzi, Isabella Mastroeni, and Elia Perantoni. 2024. Adversities in Abstract Interpretation - Ac- commodating Robustness by Abstract Interpretation. ACM Trans. Program. Lang. Syst. 46, 2 (2024), 5. https: //doi.org/10.1145/3649309

    2024 doi

  35. [44]

    Joseph A. Goguen. 1974. On Homomorphisms, Correctness, Termination, Unfoldments, and Equivalence of Flow Diagram Programs. J. Comput. Syst. Sci. 8, 3 (1974), 333–365. https://doi.org/10.1016/S0022-0000(74)80028-0

    1974 doi

  36. [45]

    Goguen and Grant Malcolm

    Joseph A. Goguen and Grant Malcolm. 1996. Algebraic semantics of imperative programs . MIT Press. Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 16. Publication date: January 2025. Calculational Design of Hyperlogics by Abstract Interpretation 16:31

    1996

  37. [46]

    Goguen and José Meseguer

    Joseph A. Goguen and José Meseguer. 1977. Correctness of Recursive Flow Diagram Programs. In MFCS (Lecture Notes in Computer Science, Vol. 53). Springer, 580–595. https://doi.org/10.1007/3-540-08353-7_183

    1977 doi

  38. [47]

    Goguen and José Meseguer

    Joseph A. Goguen and José Meseguer. 1982. Security Policies and Security Models. In S&P. IEEE Computer Society, 11–20. https://doi.org/10.1109/SP.1982.10014

    1982

  39. [48]

    Goguen and José Meseguer

    Joseph A. Goguen and José Meseguer. 1984. Unwinding and Inference Control. In S&P. IEEE Computer Society, 75–87. https://doi.org/10.1109/SP.1984.10019

    1984

  40. [49]

    Goguen, James W

    Joseph A. Goguen, James W. Thatcher, Eric G. Wagner, and Jesse B. Wright. 1977. Initial Algebra Semantics and Continuous Algebras. J. ACM 24, 1 (1977), 68–95. https://doi.org/10.1145/321992.321997

    1977

  41. [50]

    Irène Guessarian. 1978. Some Applications of Algebraic Semantics. In Mathematical Foundations of Computer Science 1978, Proceedings, 7th Symposium, Zakopane, Poland, September 4-8, 1978 (Lecture Notes in Computer Science, Vol. 64) , Józef Winkowski (Ed.). Springer, 257–266. ht...

    1978 doi

  42. [51]

    Reinhold Heckmann. 1993. Power Domains and Second-Order Predicates. Theor. Comput. Sci. 111, 1&2 (1993), 59–88. https://doi.org/10.1016/0304-3975(93)90182-S

    1993 doi

  43. [52]

    Eric C. R. Hehner. 1990. A Practical Theory of Programming. Sci. Comput. Program. 14, 2-3 (1990), 133–158. https: //doi.org/10.1016/0167-6423(90)90018-9

    1990 doi

  44. [53]

    Eric C. R. Hehner. 1993. A Practical Theory of Programming . Springer. https://doi.org/10.1007/978-1-4419-8596-5

    1993 doi

  45. [54]

    Eric C. R. Hehner. 1999. Specifications, Programs, and Total Correctness. Sci. Comput. Program. 34, 3 (1999), 191–205. https://doi.org/10.1016/S0167-6423(98)00027-6

    1999 doi

  46. [55]

    Charles Antony Richard Hoare. 1969. An Axiomatic Basis for Computer Programming. Commun. ACM 12, 10 (1969), 576–580. https://doi.org/10.1145/363235.363259

    1969

  47. [56]

    C. A. R. Hoare, Ian J. Hayes, Jifeng He, Carroll Morgan, A. W. Roscoe, Jeff W. Sanders, Ib Holm Sørensen, J. Michael Spivey, and Bernard Sufrin. 1987. Laws of Programming. Commun. ACM 30, 8 (1987), 672–686. https://doi.org/10. 1145/27651.27653

    1987

  48. [57]

    Tony Hoare. 2013. Generic Models of the Laws of Programming. In Theories of Programming and Formal Methods (Lecture Notes in Computer Science, Vol. 8051) . Springer, 213–226. https://doi.org/10.1007/978-3-642-39698-4_13

    2013 doi

  49. [58]

    Tony Hoare. 2014. Laws of Programming: The Algebraic Unification of Theories of Concurrency. In CONCUR (Lecture Notes in Computer Science, Vol. 8704) . Springer, 1–6. https://doi.org/10.1007/978-3-662-44584-6_1

    2014 doi

  50. [59]

    Tony Hoare and Stephan van Staden. 2014. The laws of programming unify process calculi. Sci. Comput. Program. 85 (2014), 102–114. https://doi.org/10.1016/J.SCICO.2013.08.012

    2014 doi

  51. [60]

    Iu. I. Ianov and M. D. Friedman. 1958. On The Equivalence and Transformation of Program Schemes. Commun. ACM 1, 10 (1958), 8–12. https://doi.org/10.1145/368924.368930

    1958

  52. [61]

    James C. King. 1976. Symbolic Execution and Program Testing. Commun. ACM 19, 7 (1976), 385–394. https: //doi.org/10.1145/360248.360252

    1976

  53. [62]

    Dexter Kozen. 1997. Kleene Algebra with Tests. ACM Trans. Program. Lang. Syst. 19, 3 (1997), 427–443. https: //doi.org/10.1145/256167.256195

    1997

  54. [63]

    Dexter Kozen. 2000. On Hoare logic and Kleene algebra with tests. ACM Trans. Comput. Log. 1, 1 (2000), 60–76. https://doi.org/10.1145/343369.343378

    2000

  55. [64]

    Xavier Leroy and Hervé Grall. 2009. Coinductive big-step operational semantics. Inf. Comput. 207, 2 (2009), 284–304. https://doi.org/10.1016/J.IC.2007.12.004

    2009 doi

  56. [65]

    Zohar Manna and Amir Pnueli. 1974. Axiomatic Approach to Total Correctness of Programs.Acta Inf. 3 (1974), 243–263. https://doi.org/10.1007/BF00288637

    1974 doi

  57. [66]

    Isabella Mastroeni and Michele Pasqua. 2017. Hyperhierarchy of Semantics - A Formal Framework for Hyperproperties Verification. In SAS (Lecture Notes in Computer Science, Vol. 10422) . Springer, 232–252. https://doi.org/10.1007/978-3- 319-66706-5_12

    2017 doi

  58. [67]

    Isabella Mastroeni and Michele Pasqua. 2018. Verifying Bounded Subset-Closed Hyperproperties. In SAS (Lecture Notes in Computer Science, Vol. 11002). Springer, 263–283. https://doi.org/10.1007/978-3-319-99725-4_17

    2018 doi

  59. [68]

    Isabella Mastroeni and Michele Pasqua. 2023. Domain Precision in Galois Connection-Less Abstract Interpretation. In Static Analysis - 30th International Symposium, SAS 2023, Cascais, Portugal, October 22-24, 2023, Proceedings (Lecture Notes in Computer Science, Vol. 14284) , M...

    2023 doi

  60. [69]

    Daryl McCullough. 1987. Specifications for Multi-Level Security and a Hook-Up Property. In S&P. IEEE Computer Society, 161–166. https://doi.org/10.1109/SP.1987.10009

    1987

  61. [70]

    Possibilistic

    John McLean. 1996. A General Theory of Composition for a Class of "Possibilistic” Properties. IEEE Trans. Software Eng. 22, 1 (1996), 53–67. https://doi.org/10.1109/32.481534

    1996 doi

  62. [71]

    O’Hearn, and Tony Hoare

    Bernhard Möller, Peter W. O’Hearn, and Tony Hoare. 2021. On Algebra of Program Correctness and Incorrectness. In RAMiCS (Lecture Notes in Computer Science, Vol. 13027) . Springer, 325–343. https://doi.org/10.1007/978-3-030-88701- 8_20 Proc. ACM Program. Lang., Vol. 9, No. POPL...

    2021 doi

  63. [72]

    James Donald Monk. 1969. Introduction to Set Theory . McGraw–Hill. http://euclid.colorado.edu/~monkd/monk11.pdf

    1969

  64. [73]

    Alan Mycroft. 1982. Abstract interpretation and optimising transformations for applicative programs . Ph. D. Dissertation. University of Edinburgh, UK. https://hdl.handle.net/1842/6602

    1982

  65. [74]

    Maurice Nivat. 1980. Non Deterministic Programs: An Algebraic Overview. In IFIP Congress. North-Holland/IFIP, 17–28

    1980

  66. [75]

    Peter W. O’Hearn. 2020. Incorrectness logic. Proc. ACM Program. Lang. 4, POPL (2020), 10:1–10:32. https://doi.org/10. 1145/3371078

    2020

  67. [76]

    Oystein Ore. 1943. Combinations of Closure Relations. Annals of Mathematics 44, 3 (July 1943), 514–533. https: //doi.org/10.2307/1968978

    1943 doi

  68. [77]

    David Michael Ritchie Park. 1969. Fixpoint Induction and Proofs of Program Properties. In Machine Intelligence Volume 5, Donald Mitchie and Bernard Meltzer (Eds.). Edinburgh Univ. Press, Chapter 3, 59–78

    1969

  69. [78]

    Gordon D. Plotkin. 1976. A Powerdomain Construction. SIAM J. Comput. 5, 3 (1976), 452–487. https://doi.org/10.1137/ 0205035

    1976

  70. [79]

    Robert Rand and Steve Zdancewic. 2015. VPHL: A Verified Partial-Correctness Logic for Probabilistic Programs. In The 31st Conference on the Mathematical Foundations of Programming Semantics, MFPS 2015, Nijmegen, The Netherlands, June 22-25, 2015 (Electronic Notes in Theoretica...

    2015 doi

  71. [80]

    Scott and Christopher Strachey

    Dana S. Scott and Christopher Strachey. 1971. Towards a Mathematical Semantics for Computer Languages . Technical Report PRG-6. Oxford University Computer Laboratory. 49 pages. https://www.cs.ox.ac.uk/files/3228/PRG06.pdf

    1971

  72. [81]

    Alfred Tarski. 1955. A Lattice Theoretical Fixpoint Theorem and Its Applications. Pacific J. of Math. 5 (1955), 285–310. https://doi.org/10.2140/pjm.1955.5.285

    1955 doi

  73. [82]

    Lena Verscht and Benjamin Lucien Kaminski. 2023. Hoare-Like Triples and Kleene Algebras with Top and Tests: Towards a Holistic Perspective on Hoare Logic, Incorrectness Logic, and Beyond. CoRR abs/2312.09662 (2023), 4 pages. https://doi.org/10.48550/ARXIV.2312.09662

    2023 doi arXiv

  74. [83]

    Morgan Ward. 1942. The Closure Operators of a Lattice. Annals of Mathematics 43, 2 (April 1942), 191–196. https: //doi.org/10.2307/1968865

    1942 doi

  75. [84]

    Peng Yan, Hanru Jiang, and Nengkun Yu. 2022. On incorrectness logic for Quantum programs. Proc. ACM Program. Lang. 6, OOPSLA1 (2022), 1–28. https://doi.org/10.1145/3527316

    2022 doi

  76. [85]

    Mingsheng Ying. 2011. Floyd-Hoare logic for quantum programs. ACM Trans. Program. Lang. Syst. 33, 6 (2011), 19:1–19:49. https://doi.org/10.1145/2049706.2049708

    2011

  77. [86]

    Steve Zdancewic and Andrew C. Myers. 2003. Observational Determinism for Concurrent Program Security. In CSFW. IEEE Computer Society, 29. https://doi.org/10.1109/CSFW.2003.1212703 Received 2024-07-08; accepted 2024-11-07 Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 16. ...

    2003 arXiv

  78. [2014]

    In POST (Lecture Notes in Computer Science, Vol

    Temporal Logics for Hyperproperties. In POST (Lecture Notes in Computer Science, Vol. 8414) . Springer, 265–284. https://doi.org/10.1007/978-3-642-54792-8_15

    doi

  79. [2023]

    An Algebra of Alignment for Relational Verification. Proc. ACM Program. Lang. 7, POPL (2023), 573–603. https://doi.org/10.1145/3571213

    2023 doi

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.