The authors show that many hyperlogics for relational program properties can be derived systematically from one parameterized algebraic semantics by abstract interpretation.
Hoare-Like Triples and Kleene Algebras with Top and Tests: Towards a Holistic Perspective on Hoare Logic, Incorrectness Logic, and Beyond
1 Pith paper cite this work. Polarity classification is still indexing.
1
Pith paper citing it
abstract
We aim at a holistic perspective on program logics, including Hoare and incorrectness logics. To this end, we study different classes of properties arising from the generalization of the aforementioned logics. We compare our results with the properties expressible in the language of Kleene algebra with top and tests.
fields
cs.LO 1years
2024 1verdicts
CONDITIONAL 1representative citing papers
citing papers explorer
-
Calculational Design of Hyperlogics by Abstract Interpretation
The authors show that many hyperlogics for relational program properties can be derived systematically from one parameterized algebraic semantics by abstract interpretation.