Program logics:

reasoning principles for high-assurance software

Xavier Leroy

Collège de France, chair of software sciences, 2020-2021

This is an English translation of Xavier Leroy's 2020-2021 lectures at Collège de France, "Logiques de programmes : quand la machine raisonne sur ses logiciels".

Abstract

Just like a mathematical logic enables us to prove properties of mathematical objects, a program logic enables us to prove properties of a computer program and of all its possible executions.

Program logics emerged in the 1960s with the seminal work of Floyd and of Hoare. Since the 2000s, program logics have tremendously progressed, with conceptual advances such as separation logics and impressive applications to the deductive verification of critical software. The course retraces these evolutions of program logics and, along with the companion seminar, presents a number of recent results in this area.

Lectures

• Introduction and course outline
• The birth of program logics
• Variables and loops: Hoare logic
• Pointers and data structures: separation logic
• Shared-memory concurrency: concurrent separation logic
• Extensions of separation logic: fractional permissions, ghost state, stored locks, ...
• Logics for weakly-consistent shared memory
• Logics for functional, higher-order languages

Companion Coq development

Seminar talks

Some talks were given in English, others in French. Video recordings and slides can be found on the main course pages.

• Loïc Correnson: Les logiques de programmes à l’épreuve du réel: tours et détours avec Frama-C/WP
• Yannick Moy: Preuve auto-active de programmes en SPARK
• Bart Jacobs: VeriFast: Semi-automated modular verification of concurrent C and Java programs using separation logic
• François Pottier: Raisonner à propos du temps en logique de séparation
• Jacques-Henri Jourdan: Protocoles personnalisés en logique de séparation: ressources fantômes et invariants dans la logique Iris
• Philippa Gardner: Gillian: Compositional Symbolic Testing and Verification