Talk "A Taxonomy of Hoare-Like Logics"

by Benjamin Lucien Kaminski

Fri, 13 June 2025 at 02:30 pm in Glasgow, Scotland

Joint work with: Lena Verscht

Abstract: We study Hoare-like logics, including partial and total correctness Hoare logic, incorrectness logic, Lisbon logic, and many others through the lens of predicate transformers à la Dijkstra and through the lens of Kleene algebra with top and tests (TopKAT). Our main goal is to give an overview – a taxonomy – of how these program logics relate, in particular under different assumptions like for example program termination, determinism, and reversibility. As a byproduct, we obtain a TopKAT characterization of Lisbon logic, which – to the best of our knowledge – is a novel result.