This description was written by a machine and published without a person checking it. It is what the agent made of this grouping, and not a statement anybody has stood behind.
Over approximate or under
A subject the papers are about. The loosest grouping, and the one to reach for last.
One connective used in four directions: a postcondition that over-approximates what a program reaches proves bad states absent, and reversing the inclusion proves them present. Collects the program logics that vary which end is fixed -- Hoare, incorrectness, and the separation-logic variants of each. Membership requires the direction of approximation to be the point of the work.
7 references
Incorrectness logic
Peter W. O'Hearn (2020) · Proceedings of the ACM on Programming Languages · Association for Computing Machinery
Iris from the ground up: A modular foundation for higher-order concurrent separation logic
Ralf Jung and others (2018) · Journal of Functional Programming · Cambridge University Press
Reverse Hoare Logic
Edsko de Vries and others (2011) · Software Engineering and Formal Methods · Springer Science+Business Media
A gentle introduction to formal verification of computer systems by abstract interpretation
Patrick Cousot and others (2010) · Logics and Languages for Reliability and Security · IOS Press
Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints
Patrick Cousot and others (1977) · 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL) · Association for Computing Machinery
Guarded commands, nondeterminacy and formal derivation of programs
Edsger W. Dijkstra (1975) · Communications of the ACM · Association for Computing Machinery
An axiomatic basis for computer programming
C. A. R. Hoare (1969) · Communications of the ACM · Association for Computing Machinery