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".
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.
Some talks were given in English, others in French. Video recordings and slides can be found on the main course pages.