P. Cousot and J. Wang, Calculational Design of Hyperlogics by Abstract Interpretation

Patrick Cousot and Jeffery Wang.
Calculational Design of Hyperlogics by Abstract Interpretation.
In Proc. ACM Program. Lang. 9, POPL, Article 16 (January 2025), 33 pages. doi.org/10.1145/3704852
Paper (33 pages): PDF (8.8 MB)
Auxiliary material (paper+appendix, 71 pages): PDF (8.6 MB)
This 75 pages file contains the paper and the appendix in a single clickable file.
The full paper is available on Zenodo DOI 10.5281/zenodo.14173477.
arXiv arxiv.org/abs/2411.11113 (with variations on fonts due to the mandatory use of pdflatex instead of xelatex)

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 ∀∃∗, ∀∀∗, and ∃∀∗ hyperlogics.
Slides of the 20mn POPL'25 presentation are available in PDF format (47.2 MB).

Presentation at POPL 2025

Recorded video of the 20mn POPL'25 presentation (YouTube 4:44:00 to 5:04:46).

\bibitem{CousotWang-POPL25-1}
Patrick Cousot and Jeffery Wang.
\newblock Calculational Design of Hyperlogics by Abstract Interpretation.
\newblock In \emph{Proc. ACM Program. Lang. 9, POPL, Article 16},
  Pages 446--478, Denver, CO, USA, January 2025. ACM Press, New York,
  NY. https://doi.org/10.1145/3704852
  

@inproceedings{CousotWang-POPL25-1,
   author =    {Cousot, P{.} and Wang, J{.}},
   title =     {Calculational Design of Hyperlogics by Abstract Interpretation},
   booktitle = {Proc. ACM Program. Lang. 9, POPL, Article 16},
   pages =     {446--478},
   address =   {Denver, CO, USA},
   publisher = {ACM Press, New York, NY},
   month =     jan,
   year =      2025,
   url =       {https://doi.org/10.1145/3704852}
}

By curiosity, I uploaded the slides PDF in DeepSeek and asked for a summary (on 01/30/2025). Here is what I got (the wrong facts are in red, the missunderstandings in blue).
``The document titled "Calculational Design of Hyperlogics by Abstract Interpretation" by Patrick Cousot and Jeffery Wang, presented at POPL 2024 in London, outlines a method for designing program transformational hyperlogics using abstract interpretation. The key points are:
- Objective: The goal is to develop a method for designing transformational hyperlogics, which are extensions of Hoare-style logics for program transformations.
- Methodology: The authors propose using structural abstractions of program semantics to calculate hyperlogics proof systems. They conclude that while it is possible, the strongest program property of interest is the collecting semantics itself, making proofs of general hyperproperties unmanageable in practice. Therefore, they suggest considering only abstract hyperproperties.
- Algebraic Semantics: The document introduces an algebraic semantics parameterized by an abstract semantic domain, providing a model of executions and the effect of primitives. This semantics is defined structurally using fixpoints.
- Property Transformer: The authors discuss how program properties can be expressed using property transformers, which are defined structurally and characterized by fixpoints.
- Hyperproperties: The document extends the discussion to hyperproperties, which are properties of sets of executions rather than individual executions. It introduces algebraic hyperproperties and hyperproperty transformers, again characterized structurally.
- Calculational Design: The authors describe a calculational design approach to derive proof systems for algebraic hyperlogics, including upper and lower algebraic hyperlogics.
- Abstractions: Due to the impracticality of proving general hyperproperties, the authors consider abstractions of the algebraic semantics, program properties, and hyperproperties. This leads to a lattice of hyperlogics with varying levels of expressiveness.
  Nothing is said about the ``Chain limit order ideal abstraction'', probably because it is mainly presented using mathematical formulas.
- Conclusion: The document concludes by summarizing the introduction of a new algebraic semantics, the design of general algebraic logics and hyperlogics, and the consideration of abstractions to make hyperlogics manageable. The authors also mention various instantiations and abstractions of the algebraic semantics, leading to complete hyperlogics.
The document provides a comprehensive framework for designing and understanding hyperlogics through abstract interpretation and algebraic semantics, with a focus on practical manageability through abstractions.''

This can be compared to the paper summary provided by reviewer B:

``This paper introduces a structural fixpoint algebraic program semantics, conceptualized as an abstract interpreter parameterized by an axiomatically defined algebraic domain. It is then instantiated to define MANY semantics and logics through various combinations of terms such as "algebraic," "semantics," "logic," "collecting," and "hyper."''

and that of reviewer C

``This paper describes an approach based on abstract interpretation to mechanically derive hyperproperties. The paper is divided into three parts: In the first part, an abstract interpreter operating by induction on the program structure is used to define its semantics. When suitably instantiated, the abstract domain yields the hyperproperties of Clarkson and Schneider. The second and third parts respectively deal with applying abstractions to these semantic properties, and proof rules for under- and over-approximating these properties.''

copyright notice
Last modified: Thursday, 30-Jan-2025 10:02:17 EST