Program Analysis
Academic year 2024/25
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.
References and material
- 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): Pointer analysis & Separation Logic (Part I)
- Click here for Lecture 4 (part I): Separation logic (Part II)
- Click here for Lecture 4 (part II): Incorrectness separation logic
- Click here for Lecture 4 (part III): Sufficient Incorrectness Separation Logic
Click here for more stuff