Everyone is well aware of the so-called Hoare correctness logic, which allows you to formally prove that a program is working correctly. What if we want to formally prove that there is a bug in the program? For example, that the program will crash if you give it a very large string as input, without specifying which string it is. It turns out that the process of proving the presence of a bug in the program can be formalized in the same way as we formalize the proof of correctness using Hoare's logic - using the "Logic of Incorrectness" In the talk we will talk about "Logic of Incorrectness": we will discuss its connection with Hoare's correctness logic, look at its natural inference and semantics, catch a couple of bugs and, finally, consider how it is related to Dynamic Logic and Relation Algebra.
Speaker: Vladimir Gladstein
Peter W. O’Hearn. 2020. Incorrectness Logic. Proc. ACM Program. Lang. 4, POPL, Article 10 (January 2020), 32 pages. https://doi.org/10.1145/3371078
The seminar will be held in google meet on Monday October 12 at 17:30 (google meet room: https://meet.google.com/myu-dhmz-gvu)