Viktor Vafeiadis

Registered user since Tue 12 Aug 2014

Name:Viktor Vafeiadis
Bio:

Viktor Vafeiadis is a tenured researcher at the Max Planck Institute for Software Systems (MPI-SWS), working on weak memory consistency and persistency. He has made numerous contributions on the semantics of weak memory consistency as well as on verification of concurrent programs with program logics and/or model checking, having published over 60 articles at top-tier venues. He got his PhD from the University of Cambridge in 2008 on concurrent program logics, for which he received the ACM SIGPLAN distinguished dissertation award. After postdoc positions at Microsoft Research and at the University of Cambridge, he joined the MPI-SWS in 2010 and got tenure in 2016.

Country:Germany
Affiliation:MPI-SWS
Research interests:Concurrency, verification, weak memory consistency, weak persistency

Contributions

SPLASH 2021 Committee Member in Review Committee within the OOPSLA-track
PLDI 2021 Committee Member in Program Committee within the PLDI-track
Author of Beyond Weak Memory Consistency: The Challenges of Memory Persistency within the Tutorials-track
PPoPP 2021 Committee Member in External Review Committee
POPL 2021 Author of PerSeVerE: Persistency Semantics for Verification under Ext4 within the POPL-track
Committee Member in Program Committee within the POPL-track
ECOOP 2020 Author of Reconciling Event Structures with Modern Multiprocessors within the Research Papers-track
Author of Reconciling Event Structures with Modern Multiprocessors within the Artifacts-track
SPLASH 2020 Author of Persistent Owicki-Gries Reasoning: A Program Logic for Reasoning about Persistent Programs on Intel-x86 within the OOPSLA-track
CoqPL 2020 Committee Member in Program Committee within the CoqPL-track
PLDI 2020 Author of Promising 2.0: Global Optimizations in Relaxed Memory Concurrency within the PLDI Research Papers-track
POPL 2020 Author of Persistency Semantics of the Intel-x86 Architecture within the Research Papers-track
SPLASH 2019 Committee Member in External Review Committee within the OOPSLA-track
Author of Effective Lock Handling In Stateless Model Checking within the OOPSLA Artifacts-track
Author of Effective Lock Handling in Stateless Model Checking within the Posters-track
Author of Effective Lock Handling in Stateless Model Checking within the OOPSLA-track
Author of Weak Persistency Semantics from the Ground Up: Formalising the Persistency Semantics of ARMv8 and Transactional Models within the OOPSLA-track
VMCAI 2019 Author of On the Semantics of Snapshot Isolation within the VMCAI 2019-track
PPoPP 2019 PC Member in Program Committee
PLDI 2019 Author of Model Checking for Weakly Consistent Libraries within the PLDI Research Papers-track
POPL 2019 Author of Bridging the Gap Between Programming Languages and Hardware Weak Memory Models within the Research Papers-track
Author of On Library Correctness under Weak Memory Consistency within the Research Papers-track
Author of Grounding Thin-Air Reads with Event Structures within the Research Papers-track
PLMW 2018 Committee Member in Organizers within the PLMW-track
SPLASH 2018 Author of Persistence Semantics for Weak Memory within the OOPSLA-track
CPP 2018 Committee Member in Program Committee within the CPP 2018-track
POPL 2018 Committee Member in Program Committee within the Research Papers-track
Author of Effective Stateless Model Checking for C/C++ Concurrency within the Artifact Evaluation-track
Author of Effective Stateless Model Checking for C/C++ Concurrency within the Research Papers-track
CPP 2017 Co-chair in Program Committee within the CPP-track
POPL 2017 Author of A Promising Semantics for Relaxed-Memory Concurrency within the POPL-track
ERC member in External Review Committee within the POPL-track
PLDI 2017 Author of Repairing Sequential Consistency in C/C++11 within the PLDI Research Papers-track
ECOOP 2017 Author of Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris within the ECOOP Research Papers-track
Author of Promising Compilation to ARMv8 POP within the ECOOP Research Papers-track
VMCAI Author of A program logic for C11 memory fences within the VMCAI-track
POPL 2016 Author of Taming Release-Acquire Consistency within the Research Papers-track
Author of Lightweight Verification of Separate Compilation within the Research Papers-track
PLDI 2015 Author of A Formal C Memory Model Supporting Integer-Pointer Casts within the Research Papers-track
Author of Verifying Read-Copy-Update in a Logic for Weak Memory within the Research Papers-track
ECOOP 2015 Author of Asynchronous Liquid Separation Types within the Research Track-track
SPLASH 2014 Author of GPS: Navigating Weak Memory with Ghosts, Protocols, and Separation within the OOPSLA-track
Presenter of GPS: Navigating Weak Memory with Ghosts, Protocols, and Separation within the OOPSLA Artifacts-track
SPLASH 2013 Author of Relaxed Separation Logic: A Program Logic for C11 Concurrency within the OOPSLA-track