Incorrectness Logic
Everyone is well aware of the socalled 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
References:
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/myudhmzgvu)
 About seminars

30 November 2020СFPQ with allpath query semantics

23 November 2020Efficient Fair Conjunction for StructurallyRecursive Relations

16 November 2020SourceTracking Unification via ContextFree Path Querying

9 November 2020Relational Synthesis for Pattern Matching

2 November 2020Definitional ProofIrrelevance without K