Abstract
In this seminar, Jacques-Henri Jourdan presented the Iris separation logic. This logic, recently developed with the help of the Coq proof assistant, enables the verification of fine-grained concurrent programs by offering the possibility of defining customized protocols for interaction between threads or between software components.
These protocols are defined using two simple, fundamental yet particularly powerful tools: invariants and phantom state. The presentation described these two concepts and the associated reasoning rules, while demonstrating their power and flexibility with the help of several examples.
