PhD Course on Program analysis

Abstract

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.

Download area for the material of the course

Lectures slides

• March 12, 11:00-13:00, Sala Seminari Est - Lecture 01 - Introduction + Fixpoint recap (R. Gori)
• March 13, 11:00-13:00, Sala Seminari Est - Lecture 02 - HL: Hoare Logic (R. Bruni)
• March 19, 11:00-13:00, Sala Seminari Est - Lecture 03 - NC: Necessary Conditions (R. Gori)
• March 20, 11:00-13:00, Sala Seminari Est - Lecture 04 - SL: Separation Logic (R. Bruni)
• March 26, 11:00-13:00, Sala Seminari Est - Lecture 05 - IL: Incorrectness Logic (A. Raad)
• March 27, 11:00-13:00, Sala Seminari Est - Lecture 06 - ISL: Incorrectness Separation Logic + UNTer (A. Raad)
• April 2, 11:00-13:00, Sala Seminari Est - Lecture 07 - SIL: Sufficient Incorrectness Logic (R. Bruni)
• April 3, 11:00-13:00, Sala Seminari Est - Lecture 18 - SepSIL: Separation SIL (R. Gori)

Main References

[HL] Krzysztof R. Apt, Ernst-Rüdiger Olderog:
Fifty years of Hoare's logic.
Formal Aspects Comput. 31(6): 751-807 (2019)

[NC] Patrick Cousot, Radhia Cousot, Manuel Fähndrich, Francesco Logozzo:
Automatic Inference of Necessary Preconditions.
VMCAI 2013: 128-148 (2013)

[SL] Peter W. O'Hearn, John C. Reynolds, Hongseok Yang:
Local Reasoning about Programs that Alter Data Structures.
CSL 2001: 1-19 (2001)

[IL] Peter W. O'Hearn:
Incorrectness logic.
Proc. ACM Program. Lang. 4(POPL): 10:1-10:32 (2020)

[ISL] Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter W. O'Hearn, Jules Villard:
Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic.
CAV (2) 2020: 225-252 (2020)

[UNTer] Azalea Raad, Julien Vanegue, Peter O'Hearn:
Non-Termination Proving at Scale.
Proc. ACM Program. Lang. 8(OOPSLA2): 246-274 (2024)

[SIL + SepSIL] Flavio Ascari, Roberto Bruni, Roberta Gori, Francesco Logozzo:
Sufficient Incorrectness Logic: SIL and Separation SIL.
CoRR abs/2310.18156 (2023)

Historical References

Alan Turing: Checking a large routine.
Report of a Conference on High Speed Automatic Calculating Machines, pp.67-69 (1949)
See also:
F. L. Morris and C. B. Jones:
An Early Program Proof by Alan Turing.
Annals of the History of Computing, vol. 6, no. 2, pp. 139-143 (1984)

R. W. Floyd:
Assigning meanings to programs.
Proceedings of the American Mathematical Society Symposia on Applied Mathematics. Vol. 19, pp. 19–31 (1967)

C. A. R. Hoare:
An axiomatic basis for computer programming.
Communications of the ACM. 12 (10): 576–580 (1969)