Viktor Vafeiadis receives Robin Milner Young Researcher Award

MPI-SWS faculty member Viktor Vafeiadis has received the 2022 Robin Milner Young Researcher Award, which is given by ACM SIGPLAN to recognize outstanding contributions by young investigators in the area of programming languages. The award citation reads as follows:
"Viktor has become a world leader in semantics and verification research. His body of work includes fundamental and influential contributions to the study of concurrency, in particular separation logic and relaxed memory models. His landmark doctoral thesis developed RGSep,
...MPI-SWS faculty member Viktor Vafeiadis has received the 2022 Robin Milner Young Researcher Award, which is given by ACM SIGPLAN to recognize outstanding contributions by young investigators in the area of programming languages. The award citation reads as follows:
"Viktor has become a world leader in semantics and verification research. His body of work includes fundamental and influential contributions to the study of concurrency, in particular separation logic and relaxed memory models. His landmark doctoral thesis developed RGSep, the first extension of concurrent separation logic to support formal proofs about fine-grained concurrent algorithms. His work on Cave presented the first fully automatic verifier for establishing linearizability of a class of concurrent data structures, including ones with non-fixed linearization points. His work on CompCertTSO presented the first verified compiler for a concurrent language under a relaxed memory model. He developed the first direct (and mechanized) proof of soundness for concurrent separation logic (CSL) based on operational semantics—beautifully simple compared to prior proofs and a key enabler for proving soundness of more advanced program logics like CAP and Iris. He developed the first separation logic for the C/C++ relaxed memory model—a tour-de-force achievement compared to the standard CSL which assumes sequential consistency. This spawned a whole body of work on modular verification of concurrent data structures under relaxed memory models. His work has found and corrected a number of serious flaws in the C/C++ concurrency model, which led to changes in the C++ standard. And his "promising" semantics for relaxed-memory concurrency offered one of the first viable solutions to the 30-year-old "out-of-thin-air" problem and spawned much follow-on work. His work on GenMC presented the first efficient model checkers for relaxed-memory C/C++ programs with optimality guarantees about their state space exploration. Recent work together with his postdoc Azalea Raad (now faculty at Imperial), presented the first "persistency semantics" for non-volatile memory on multicore architectures. Viktor is not only highly-cited and incredibly prolific—he is also a true pioneer, repeatedly exploring dauntingly technical problems in the semantics and verification of concurrent programs before others dare to try."
This award makes MPI-SWS the only institution in the world to boast two recipients of the SIGPLAN Milner award among its faculty.