Speaker
Viktor Vafeiadis is a researcher at MPI-SWS, working on programming languages and verification. He has been focusing more particularly on verified compilation, and logics for various flavors of concurrent programs.
Abstract
The course will cover the foundations of reasoning about the correctness of concurrent programs using concurrent program logics. We will start with the basic reasoning principles of separation, interference, and auxiliary/ghost variables, as encompassed in the classical Owicki-Gries method, in rely/guarantee reasoning and in concurrent separation logic. Then, we will move on to more modern logics, such as RGSep and CAP that combine rely/guarantee thinking with separation logic, and to the Iris framework that can encode most of the other program logics. We will finish with an outlook as to how these basic reasoning principles can be used to reason about programs running under weak memory consistency.
Slides: part 1 (Owicki-Gries), part 2a (separation logic), part 2b (soundness), part 3a (RGsep), part 3b (iris), part 4 (RPL).