A Taxonomy of Hoare-Like Logics - Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests

This 20-minute conference talk from POPL 2025 presents a comprehensive taxonomy of Hoare-like logics, examining various program logics through predicate transformers and Kleene algebra with top and tests (TopKAT). Explore how researchers Lena Verscht and Benjamin Lucien Kaminski systematically analyze the relationships between different program logics including partial and total correctness Hoare logic, incorrectness logic, and Lisbon logic. Discover how these logics relate under varying assumptions such as program termination, determinism, and reversibility. The presentation introduces a novel TopKAT characterization of Lisbon logic as a significant contribution to the field. This ACM SIGPLAN-sponsored talk was delivered at the POPL 2025 conference, with the full research article available through DOI: 10.1145/3704896.