Incorrectness Logic

Program correctness and incorrectness are two sides of the same coin. As a programmer, even if you would like to have correctness, you might find yourself spending most of your time reasoning about incorrectness. This includes informal reasoning that people do while looking at or thinking about their code, as well as that supported by automated testing and static analysis tools. This talk describes a simple logic for program incorrectness which is, in a sense, the other side of the coin to Hoare?s logic of correctness.

Peter O’Hearn is a Research Scientist at Facebook and a Professor at University College London. His research has been in program logic, semantics and applications. With John Reynolds, Peter devised separation logic, a theory which opened up new practical possibilities for program proof, including the technology which led to the Infer program analyzer developed by Peter’s team at Facebook, which is used as well at Amazon, Mozilla, Spotify and other companies. Peter is a Fellow of the Royal Society (elected in 2018), a Fellow of the Royal Academy of Engineering (2016), he has received a number of awards for his work including the 2016 CAV Award and the 2016 Godel Prize. He received an honorary doctorate from Dalhousie University in 2018.