A Taxonomy of Hoare-Like Logics
Speaker: Yao Li
Yao Li (He/Him) is an assistant professor of computer science at Portland State University. His main research area is in functional programming, interactive theorem proving, and program verification. His current research focuses on using interactive theorem provers to verify existing programs written without verification in mind. He obtained his Ph.D. from the University of Pennsylvania in 2022, under the supervision of Stephanie Weirich.
Abstract
In this talk, I will present a paper I recently read and really liked. The paper is "A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests" (https://doi.org/10.1145/3704896). I have always been interested in incorrectness logic, but at the same time, I find it counterintuitive in a few ways; and it puzzles me whether incorrectness is indeed a dual of Hoare logic. This paper presents a very simple and clean framework for considering all these---in fact, it goes further by identifying 8 different kinds of predicate transformers and 16 different Hoare-like logics built upon them. I will discuss this framework in my talk.