JetBrains Research unites scientists working in challenging new disciplines

Incorrectness Logic

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.

The seminar will be held in google meet on Monday October 12 at 17:30 (google meet room: