Peter O’Hearn’s recent Incorrectness logic is a program logic similar to Hoare Logic which is intended for showing the presence, rather than the absence of bugs. Dynamic logic is a type of modal logic in which Hoare logic can be embedded, and O’Hearn conjectures that a similar characterisation can be done for Incorrectness logic. This project would be to define this characterisation, and formalise and evaluate the relationship between Incorrectness logic and other established tools for reasoning about programs, including temporal logic, Kleene algebrae with tests, and classical Hoare logic.
Optionally, the student may wish to mechanise their results in a proof assistant such as Isabelle/HOL.
Skills required: Logic, mathematics, (optional) proof assistants.