Program logic : when the machine reasons about its software

Just as a mathematical logic can be used to demonstrate properties of mathematical objects, a program logic can be used to demonstrate properties of a computer program and all its possible executions. Program logics first appeared in the 1960s, with the seminal work of Floyd and Hoare, and have developed enormously since the 2000s, with conceptual advances such as separation logics and fine applications to deductive verification of mission-critical software. The lecture will trace this evolution of ideas and, in conjunction with the seminar, present a number of recent results in the field.