Viktor Vafeiadis
Max Planck Institute for Software Systems (MPI-SWS)
Automated Verification of Low-Level Concurrent C/C++ Components
This talk will discuss model checking and how it can be applied to verify concurrent C/C++ components. Model checking is an automatic verification technique that has been successfully applied in industry to validate hardware and sequential software components. Applying model checking to concurrent programs, however, is much harder because concurrency induces an enormous space of possible program behaviours that need to be checked for their correctness. Nevertheless, we show that it is possible to do so and, moreover, that it is also useful in practice.
Viktor Vafeiadis is a tenured researcher at the Max Planck Institute for Software Systems (MPI-SWS), working on weak memory consistency and persistency. After getting his PhD from the University of Cambridge in 2008, he worked as a postdoc at Microsoft Research and at the University of Cambridge. He joined MPI-SWS in 2010, and got tenure in 2016. He is known for his work on concurrent program logics, for which he received the ACM SIGPLAN distinguished dissertation award, on weak memory models, and recently on weak persistency, for which he was awarded an ERC Consolidator Grant.
Homepage: https://people.mpi-sws.org/~viktor/
