Program analysis:
from proving correctness to proving incorrectness

Abstract

This short 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

• Lecture 01 - Introduction
• Lecture 02 - Hoare Logic (HL)
• Lecture 03 - Incorrectness Logic (IL)
• Lecture 04+05 - Abstract Interpretation (Abs.Int.)
• Lecture 06 - Local Completeness Logic (LCL)
• Lecture 07 - Forward and backward repair (Repair)
• Lecture 08 - Necessary Conditions and Sufficient Incorrectness Logic (NC and SIL)
• Lecture 09 - Separation Logic (SL)
• Lecture 10 - Incorrectness Separation Logic (ISL)
• Lecture 11 - Separation SIL (SepSIL)

Exam Questions

• Special prize question Send your solution to roberto.bruni@unipi.it and roberta.gori@unipi.it with subject BISS2024 before Thursday March 14, at 13:00
• Exam questions Please register for the exam using this form, then solve as many questions as you can from number 1 to 16 and send your solutions to roberto.bruni@unipi.it and roberta.gori@unipi.it with subject BISS2024-EXAM

Main References

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

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

[Abs.Int.] Xavier Rival, Kwangkeun Yi:
Introduction to Static Analysis: An Abstract Interpretation Perspective.
The MIT Press. ISBN 9780262043410 (2020)

[LCL] Roberto Bruni, Roberto Giacobazzi, Roberta Gori, Francesco Ranzato:
A Correctness and Incorrectness Program Logic.
J. ACM 70(2): 15:1-15:45 (2023)

[Repair] Roberto Bruni, Roberto Giacobazzi, Roberta Gori, Francesco Ranzato:
Abstract interpretation repair.
PLDI 2022: 426-441 (2022)

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

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

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

[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:
Compositional Non-Termination Proving.
Preprint (2024)

Additional References

[Abs.Int.] Patrick Cousot:
Principles of Abstract Interpretation.
The MIT Press. ISBN 9780262044905 (2021)

[Abs.Int.] Roberto Bruni, Roberto Giacobazzi, Roberta Gori, Isabel Garcia-Contreras, Dusko Pavlovic:
Abstract extensionality: on the properties of incomplete abstract interpretations.
Proc. ACM Program. Lang. 4(POPL): 28:1-28:28 (2020)

[Abs.Int.] Roberto Bruni, Roberta Gori, Nicolas Manini:
Deciding Program Properties via Complete Abstractions on Bounded Domains.
SAS 2022: 175-200 (2022)

[Abs.Int.] Flavio Ascari, Roberto Bruni, Roberta Gori:
Limits and difficulties in the design of under-approximation abstract domains.
FoSSaCS 2022: 21-39 (2022)

[CEGAR] Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith:
Counterexample-guided abstraction refinement for symbolic model checking.
J. ACM 50(5): 752-794 (2003)

[LCL] Flavio Ascari, Roberto Bruni, Roberta Gori:
Logics for Extensional, Locally Complete Analysis via Domain Refinements.
ESOP 2023: 1-27 (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)