Emilio's web page

Advanced course
Lecturer: Roberto Bruni, University of Pisa, IT
This course offers a focused exploration of formal methods in software development, with some emphasis on the shift of perspectives after Peter O’Hearn’s influential paper on incorrectness logic. Instead of exploiting over-approximations to prove program correctness like done with classical formal methods, incorrectness reasoning exploits under-approximations for exposing true bugs. The overall goal of incorrectness methods is to develop principled techniques to assist programmers with timely feedback about the presence of true errors, with few or zero false alarms.
The course will overview different approaches, like program logics, pointer analysis, and abstract interpretation, for both over- and under-approximation, as well as their combination.

Click here for Lecture 1 (part I): Introducing the course with riddles, intuitions and rigour
Click here for Lecture 1 (part II): A brief history, Turing, Floyd, Hoare, Naur…and then Hoare’s logic
Click here for Lecture 2 (part I): Correctness logic, invariants, validity, soundness, completeness
Click here for Lecture 2 (part II): Incorrectness logic, its relations with Hoare’s logic, validity, soundness, completeness
Click here for Lecture 3 (part I): Necessary conditions
Click here for Lecture 3 (part II): Sufficient Incorrectness logic
Click here for Lecture 3 (part III): Separation logic

Program Analysis

References and material