references.bib

@inproceedings{Cousot77,
  author = {Cousot, Patrick and Cousot, Radhia},
  title = {Abstract interpretation: a unified lattice model for static analysis 
    of programs by construction or approximation of fixpoints},
  year = {1977},
  isbn = {9781450373500},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  url = {https://doi.org/10.1145/512950.512973},
  doi = {10.1145/512950.512973},
  abstract = {A program denotes computations in some universe of objects. 
    Abstract interpretation of programs consists in using that denotation to 
    describe computations in another universe of abstract objects, so that the 
    results of abstract execution give some information on the actual 
    computations. An intuitive example (which we borrow from Sintzoff [72]) is 
    the rule of signs. The text -1515 * 17 may be understood to denote 
    computations on the abstract universe {(+), (-), (±)} where the semantics 
    of arithmetic operators is defined by the rule of signs. The abstract 
    execution -1515 * 17 → -(+) * (+) → (-) * (+) → (-), proves that 
    -1515 * 17 is a negative number. Abstract interpretation is concerned by a 
    particular underlying structure of the usual universe of computations (the 
    sign, in our example). It gives a summary of some facets of the actual 
    executions of a program. In general this summary is simple to obtain but 
    inaccurate (e.g. -1515 + 17 → -(+) + (+) → (-) + (+) → (±)). Despite its 
    fundamentally incomplete results abstract interpretation allows the 
    programmer or the compiler to answer questions which do not need full 
    knowledge of program executions or which tolerate an imprecise answer, 
    (e.g. partial correctness proofs of programs ignoring the termination 
    problems, type checking, program optimizations which are not carried in the 
    absence of certainty about their feasibility, …).},
  booktitle = {Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles
    of Programming Languages},
  pages = {238–252},
  numpages = {15},
  location = {Los Angeles, California},
  series = {POPL '77}
}

@techreport{Scott70,
  title = "OUTLINE OF A MATHEMATICAL THEORY OF COMPUTATION",
  author = "Dana Scott",
  year = "1970",
  institution = "OUCL",
  month = "November",
  number = "PRG02",
  pages = "30",
}


@unpublished{Dijkstra74,
  author = "Edsger W. Dijkstra",
  title = "Guarded commands, non-determinacy and a calculus for the derivation 
   of programs",
  month = jun,
  year = "1974",
  note = "circulated privately",
  url = "http://www.cs.utexas.edu/users/EWD/ewd04xx/EWD418.PDF",
}

@article{Cousot12,
  author = {Cousot, Patrick and Cousot, Radhia and Logozzo, Francesco and 
    Barnett, Michael},
  year = {2012},
  month = {10},
  pages = {},
  title = {An Abstract Interpretation Framework for Refactoring with 
    Application to Extract Methods with Contracts},
  volume = {47},
  isbn = {978-1-4503-1561-6},
  journal = {ACM SIGPLAN Notices},
  doi = {10.1145/2384616.2384633}
}


@article{Cook78,
  author = {Cook, Stephen A.},
  title = {Soundness and Completeness of an Axiom System for Program 
    Verification},
  journal = {SIAM Journal on Computing},
  volume = {7},
  number = {1},
  pages = {70-90},
  year = {1978},
  doi = {10.1137/0207005},
  URL = { https://doi.org/10.1137/0207005 },
  eprint = { https://doi.org/10.1137/0207005 },
  abstract = { A simple ALGOL-like language is defined which includes 
    conditional, while, and procedure call statements as well as blocks. A 
    formal interpretive semantics and a Hoare style axiom system are given for 
    the language. The axiom system is proved to be sound, and in a certain sense 
    complete, relative to the interpretive semantics. The main new results are 
    the completeness theorem, and a careful treatment of the procedure call 
    rules for procedures with global variables in their declarations. }
}

@article{Fischer79,
  title = {Propositional dynamic logic of regular programs},
  journal = {Journal of Computer and System Sciences},
  volume = {18},
  number = {2},
  pages = {194-211},
  year = {1979},
  issn = {0022-0000},
  doi = {https://doi.org/10.1016/0022-0000(79)90046-1},
  url = {https://www.sciencedirect.com/science/article/pii/0022000079900461},
  author = {Michael J. Fischer and Richard E. Ladner},
  abstract = {We introduce a fundamental propositional logical system based on 
    modal logic for describing correctness, termination and equivalence of 
    programs. We define a formal syntax and semantics for the propositional 
    dynamic logic of regular programs and give several consequences of the 
    definition. Principal conclusions are that deciding satisfiability of length 
    n formulas requires time dn/logn for some d > 1, and that satisfiability 
    can be decided in nondeterministic time cn for some c. We provide 
    applications of the decision procedure to regular expressions, Ianov schemes, 
    and classical systems of modal logic.}
}

@article{Hoare69,
  author = {Hoare, C. A. R.},
  title = {An axiomatic basis for computer programming},
  year = {1969},
  issue_date = {Oct. 1969},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {12},
  number = {10},
  issn = {0001-0782},
  url = {https://doi.org/10.1145/363235.363259},
  doi = {10.1145/363235.363259},
  abstract = {In this paper an attempt is made to explore the logical foundations of computer programming by use of techniques which were first applied in the study of geometry and have later been extended to other branches of mathematics. This involves the elucidation of sets of axioms and rules of inference which can be used in proofs of the properties of computer programs. Examples are given of such axioms and rules, and a formal proof of a simple theorem is displayed. Finally, it is argued that important advantage, both theoretical and practical, may follow from a pursuance of these topics.},
  journal = {Commun. ACM},
  month = {oct},
  pages = {576–580},
  numpages = {5},
  keywords = {axiomatic method, formal language definition, machine-independent programming, program documentation, programming language design, theory of programming' proofs of programs}
}


@Inbook{Floyd93,
  author="Floyd, Robert W.",
  editor="Colburn, Timothy R.
  and Fetzer, James H.
  and Rankin, Terry L.",
  title="Assigning Meanings to Programs",
  bookTitle="Program Verification: Fundamental Issues in Computer Science",
  year="1993",
  publisher="Springer Netherlands",
  address="Dordrecht",
  pages="65--81",
  abstract="This paper attempts to provide an adequate basis for formal definitions of the meanings of programs in appropriately defined programming languages, in such a way that a rigorous standard is established for proofs about computer programs, including proofs of correctness, equivalence, and termination. The basis of our approach is the notion of an interpretation of a program: that is, an association of a proposition with each connection in the flow of control through a program, where the proposition is asserted to hold whenever that connection is taken. To prevent an interpretation from being chosen arbitrarily, a condition is imposed on each command of the program. This condition guarantees that whenever a command is reached by way of a connection whose associated proposition is then true, it will be left (if at all) by a connection whose associated proposition will be true at that time. Then by induction on the number of commands executed, one sees that if a program is entered by a connection whose associated proposition is then true, it will be left (if at all) by a connection whose associated proposition will be true at that time. By this means, we may prove certain properties of programs, particularly properties of the form: `If the initial values of the program variables satisfy the relation Rl, the final values on completion will satisfy the relation R2'.",
  isbn="978-94-011-1793-7",
  doi="10.1007/978-94-011-1793-7_4",
  url="https://doi.org/10.1007/978-94-011-1793-7_4"
}


@InProceedings{Moller21,
  author="M{\"o}ller, Bernhard
  and O'Hearn, Peter
  and Hoare, Tony",
  editor="Fahrenberg, Uli
  and Gehrke, Mai
  and Santocanale, Luigi
  and Winter, Michael",
  title="On Algebra of Program Correctness and Incorrectness",
  booktitle="Relational and Algebraic Methods in Computer Science",
  year="2021",
  publisher="Springer International Publishing",
  address="Cham",
  pages="325--343",
  abstract="Variants of Kleene algebra have been used to provide foundations of reasoning about programs, for instance by representing Hoare Logic (HL) in algebra. That work has generally emphasised program correctness, i.e., proving the absence of bugs. Recently, Incorrectness Logic (IL) has been advanced as a formalism for the dual problem: proving the presence of bugs. IL is intended to underpin the use of logic in program testing and static bug finding. Here, we use a Kleene algebra with diamond operators and countable joins of tests, which embeds IL, and which also is complete for reasoning about the image of the embedding. Next to embedding IL, the algebra is able to embed HL, and allows making connections between IL and HL specifications. In this sense, it unifies correctness and incorrectness reasoning in one formalism.",
  isbn="978-3-030-88701-8"
}


@INPROCEEDINGS{Clarkson08,
  author={Clarkson, Michael R. and Schneider, Fred B.},
  booktitle={2008 21st IEEE Computer Security Foundations Symposium}, 
  title={Hyperproperties}, 
  year={2008},
  volume={},
  number={},
  pages={51-65},
  keywords={Safety;Information security;Topology;Delay effects;Computer 
    security;Computer science;Writing;Security policies;safety;liveness},
  doi={10.1109/CSF.2008.7}
}

@inproceedings{Mounir17,
  author = {Assaf, Mounir and Naumann, David A. and Signoles, Julien and Totel, 
    \'{E}ric and Tronel, Fr\'{e}d\'{e}ric},
  title = {Hypercollecting semantics and its application to static analysis of 
    information flow},
  year = {2017},
  isbn = {9781450346603},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  url = {https://doi.org/10.1145/3009837.3009889},
  doi = {10.1145/3009837.3009889},
  abstract = {We show how static analysis for secure information flow can be 
    expressed and proved correct entirely within the framework of abstract 
    interpretation. The key idea is to define a Galois connection that directly 
    approximates the hyperproperty of interest. To enable use of such Galois 
    connections, we introduce a fixpoint characterisation of hypercollecting 
    semantics, i.e. a "set of sets" transformer. This makes it possible to 
    systematically derive static analyses for hyperproperties entirely within 
    the calculational framework of abstract interpretation. We evaluate this 
    technique by deriving example static analyses. For qualitative information 
    flow, we derive a dependence analysis similar to the logic of Amtoft and 
    Banerjee (SAS '04) and the type system of Hunt and Sands (POPL '06). For 
    quantitative information flow, we derive a novel cardinality analysis that 
    bounds the leakage conveyed by a program instead of simply deciding whether 
    it exists. This encompasses problems that are hypersafety but not k-safety. 
    We put the framework to use and introduce variations that achieve precision 
    rivalling the most recent and precise static analyses for information flow.},
  booktitle = {Proceedings of the 44th ACM SIGPLAN Symposium on Principles of 
    Programming Languages},
  pages = {874–887},
  numpages = {14},
  keywords = {abstract interpretation, hyperproperties, information flow, static analysis},
  location = {Paris, France},
  series = {POPL '17}
}

@InProceedings{Mastroeni18,
  author="Mastroeni, Isabella and Pasqua, Michele",
  editor="Podelski, Andreas",
  title="Verifying Bounded Subset-Closed Hyperproperties",
  booktitle="Static Analysis",
  year="2018",
  publisher="Springer International Publishing",
  address="Cham",
  pages="263--283",
  abstract="Hyperproperties are quickly becoming very popular in the context of 
    systems security, due to their expressive power. They differ from classic 
    trace properties since they are represented by sets of sets of executions 
    instead of sets of executions. This allows us, for instance, to capture 
    information flow security specifications, which cannot be expressed as trace 
    properties, namely as predicates over single executions. In this work, we 
    reason about how it is possible to move standard abstract 
    interpretation-based static analysis methods, designed for trace properties, 
    towards the verification of hyperproperties. In particular, we focus on the 
    verification of bounded subset-closed hyperproperties which are easier to 
    verify than generic hyperproperties. It turns out that a lot of interesting 
    specifications (e.g., Non-Interference) lie in this category.",
  isbn="978-3-319-99725-4"
}

@unknown{Darnier2023,
  author = {Dardinier, Thibault and Müller, Peter},
  year = {2023},
  month = {01},
  pages = {},
  title = {Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version)},
  doi = {10.48550/arXiv.2301.10037}
}

@article{Brookes16,
  author = {Brookes, Stephen and O'Hearn, Peter W.},
  title = {Concurrent separation logic},
  year = {2016},
  issue_date = {July 2016},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {3},
  number = {3},
  url = {https://doi.org/10.1145/2984450.2984457},
  doi = {10.1145/2984450.2984457},
  abstract = {Concurrent Separation Logic (CSL) was originally advanced in 
    papers of the authors published in Theoretical Computer Science for John
    Reynolds's 70th Birthday Festschrift (2007). Preliminary versions appeared 
    as invited papers in the CONCUR'04 conference proceedings. Foundational work
    leading to these papers began in 2002. Since then there have been significant
    developments stemming from CSL, both in theoretical and practical research.
    In this retrospective paper we describe the main ideas that underpin CSL,
    placing these ideas into historical context by summarizing the prevailing
    tendencies in concurrency verification and programming language semantics
    when the logic was being invented in 2002-2003. We end with a snapshot of 
    the state-of-the-art as of 2016. Along the way we describe some of the main
    developments in the intervening period, and we attempt to classify the work
    that has been done, along broad lines. While we do not intend an exhaustive
    survey, we do hope to provide some general perspective on what has been
    achieved in the field, what remains to be done, and directions for future
    work.}, 
  journal = {ACM SIGLOG News},
  month = {aug},
  pages = {47–65},
  numpages = {19}
}

@article{Kozen97,
  author = {Kozen, Dexter},
  title = {Kleene algebra with tests},
  year = {1997},
  issue_date = {May 1997},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {19},
  number = {3},
  issn = {0164-0925},
  url = {https://doi.org/10.1145/256167.256195},
  doi = {10.1145/256167.256195},
  abstract = {We introduce Kleene algebra with tests, an equational system for manipulating programs. We give a purely equational proof, using Kleene algebra with tests and commutativity conditions, of the following classical result: every while program can be simulated by a while program can be simulated by a while program with at most one while loop. The proof illustrates the use of Kleene algebra with tests and commutativity conditions in program equivalence proofs.},
  journal = {ACM Trans. Program. Lang. Syst.},
  month = {may},
  pages = {427–443},
  numpages = {17},
  keywords = {Kleene algebra, dynamic logic, specification}
}

@article{OHearn19,
  author = {O'Hearn, Peter W.},
  title = {Incorrectness logic},
  year = {2019},
  issue_date = {January 2020},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {4},
  number = {POPL},
  url = {https://doi.org/10.1145/3371078},
  doi = {10.1145/3371078},
  abstract = {Program correctness and incorrectness are two sides of the same
    coin. As a programmer, even if you would like to have correctness, you might
    find yourself spending most of your time reasoning about incorrectness. This
    includes informal reasoning that people do while looking at or thinking about
    their code, as well as that supported by automated testing and static
    analysis tools. This paper describes a simple logic for program incorrectness
    which is, in a sense, the other side of the coin to Hoare's logic of
    correctness.},
  journal = {Proc. ACM Program. Lang.},
  month = {dec},
  articleno = {10},
  numpages = {32},
  keywords = {none}
}


@InProceedings{Cousot13,
  author="Cousot, Patrick
  and Cousot, Radhia
  and F{\"a}hndrich, Manuel
  and Logozzo, Francesco",
  editor="Giacobazzi, Roberto
  and Berdine, Josh
  and Mastroeni, Isabella",
  title="Automatic Inference of Necessary Preconditions",
  booktitle="Verification, Model Checking, and Abstract Interpretation",
  year="2013",
  publisher="Springer Berlin Heidelberg",
  address="Berlin, Heidelberg",
  pages="128--148",
  abstract="We consider the problem of automatic precondition inference. We
  argue that the common notion of sufficient precondition inference (i.e.,
  under which precondition is the program correct?) imposes too large a burden
  on callers, and hence it is unfit for automatic program analysis. Therefore,
  we define the problem of necessary precondition inference (i.e., under which
  precondition, if violated, will the program always be incorrect?). We
  designed and implemented several new abstract interpretation-based analyses
  to infer atomic, disjunctive, universally and existentially quantified
  necessary preconditions.",
  isbn="978-3-642-35873-9"
}

@inproceedings{Martin06,
  author = {Martin, Ursula and Mathiesen, Erik and Oliva, Paulo},
  year = {2006},
  month = {01},
  pages = {501-515},
  title = {Hoare Logic in the Abstract},
  volume = {4207},
  isbn = {978-3-540-45458-8},
  doi = {10.1007/11874683_33}
}

@misc{Ascari24,
  title={Sufficient Incorrectness Logic: SIL and Separation SIL}, 
  author={Flavio Ascari and Roberto Bruni and Roberta Gori and Francesco Logozzo},
  year={2024},
  eprint={2310.18156},
  archivePrefix={arXiv},
}

@phdthesis{Kaminski19,
  author = {Kaminski, Benjamin},
  year = {2019},
  month = {02},
  pages = {},
  title = {Advanced Weakest Precondition Calculi for Probabilistic Programs},
  doi = {10.18154/RWTH-2019-01829}
}

@article{Zhang22,
  author = {Zhang, Linpeng and Kaminski, Benjamin Lucien},
  title = {Quantitative strongest post: a calculus for reasoning about the flow of quantitative information},
  year = {2022},
  issue_date = {April 2022},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {6},
  number = {OOPSLA1},
  url = {https://doi.org/10.1145/3527331},
  doi = {10.1145/3527331},
  abstract = {We present a novel strongest-postcondition-style calculus for
  quantitative reasoning about non-deterministic programs with loops. Whereas
  existing quantitative weakest pre allows reasoning about the value of a
  quantity after a program terminates on a given initial state, quantitative
  strongest post allows reasoning about the value that a quantity had before
  the program was executed and reached a given final state. We show how
  strongest post enables reasoning about the flow of quantitative information
  through programs. Similarly to weakest liberal preconditions, we also develop
  a quantitative strongest liberal post. As a byproduct, we obtain the entirely
  unexplored notion of strongest liberal postconditions and show how these
  foreshadow a potential new program logic - partial incorrectness logic -
  which would be a more liberal version of O'Hearn's recent incorrectness
  logic.}, 
  journal = {Proc. ACM Program. Lang.},
  month = {apr},
  articleno = {87},
  numpages = {29},
  keywords = {Weakest Precondition, Strongest Postcondition, Quantitative Verification, Incorrectness Logic}
}

@article{Zilberstein23,
  author = {Zilberstein, Noam and Dreyer, Derek and Silva, Alexandra},
  title = {Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning},
  year = {2023},
  issue_date = {April 2023},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {7},
  number = {OOPSLA1},
  url = {https://doi.org/10.1145/3586045},
  doi = {10.1145/3586045},
  abstract = {Program logics for bug-finding (such as the recently introduced
  Incorrectness Logic) have framed correctness and incorrectness as dual
  concepts requiring different logical foundations. In this paper, we argue
  that a single unified theory can be used for both correctness and
  incorrectness reasoning. We present Outcome Logic (OL), a novel
  generalization of Hoare Logic that is both monadic (to capture computational
  effects) and monoidal (to reason about outcomes and reachability). OL
  expresses true positive bugs, while retaining correctness reasoning abilities
  as well. To formalize the applicability of OL to both correctness and
  incorrectness, we prove that any false OL specification can be disproven in
  OL itself. We also use our framework to reason about new types of
  incorrectness in nondeterministic and probabilistic programs. Given these
  advances, we advocate for OL as a new foundational theory of correctness and
  incorrectness.}, 
  journal = {Proc. ACM Program. Lang.},
  month = {apr},
  articleno = {93},
  numpages = {29},
  keywords = {Program Logics, Incorrectness Reasoning, Hoare Logic}
}


@book{Gratzer11,
  title={Lattice Theory: Foundation},
  author={Gr{\"a}tzer, G.},
  isbn={9783034800181},
  lccn={2011921250},
  series={SpringerLink : B{\"u}cher},
  year={2011},
  publisher={Springer Basel}
}


@book{Birkhoff40,
  title={Lattice Theory},
  author={Birkhoff, G.},
  number={v. 25,pt. 2},
  isbn={9780821810255},
  lccn={66023707},
  series={American Mathematical Society colloquium publications},
  year={1940},
  publisher={American Mathematical Society}
}


@book{Cousot21,
  title={Principles of Abstract Interpretation},
  author={Cousot, P.},
  isbn={9780262044905},
  lccn={2020041256},
  year={2021},
  publisher={MIT Press}
}


@INPROCEEDINGS{Gougen82,
  author={Goguen, J. A. and Meseguer, J.},
  booktitle={1982 IEEE Symposium on Security and Privacy}, 
  title={Security Policies and Security Models}, 
  year={1982},
  volume={},
  number={},
  pages={11-11},
  keywords={Computational modeling;Automata;Finite element methods;Mathematical model;Data models;Computers;Message systems},
  doi={10.1109/SP.1982.10014}
}