Viktor Vafeiadis / Βίκτωρ Βαφειάδης
Faculty (tenure-track), Max Planck Institute for Software Systems (MPI-SWS)

MPI-SWS, Paul-Ehrlich-Str. 26
67663 Kaiserslautern, Germany
viktor [at] mpi-sws [dot] org

Since October 2010, I am a tenure-track researcher at MPI-SWS working on software verification. Previously, I was a post-doctoral researcher at the University of Cambridge Computer Laboratory and Microsoft Research Cambridge. My undergraduate studies and PhD were both at the University of Cambridge.

Research

I am generally interested in program analysis/verification, programming languages and concurrency. My main focus is on developing program logics and static analyses for reasoning about concurrent programs and on compiler verification.

Tutorial on rely/guarantee thinking and separation logic at FM 2011

Program logics I have (co)developed the following program logics:

• RGSep, a combination rely/guarantee and separation logic; and
• Deny-Guarantee, another combination of RG and SL allowing dynamically splitting of interference.

I also have come up with a simple soundness proof for concurrent separation logic.

Software

• SmallfootRG: a verification tool that proves safety properties of concurrent programs.
• Cave: a verification tool for proving linearizability of concurrent programs.
• CompcertTSO: a verified compiler from Clight-TSO to x86-TSO.
• Paco: a Coq library for parameterized coinduction.

Program committees POPL 2014, Coq 2013, ICFEM 2013, SEFM 2013, PCI 2013, TASE 2013, PLDI 2013 (ERC), POPL 2013 (ERC), ICFEM 2012, SEFM 2012, CPP 2011, APLAS 2011, ICFEM 2011, CAV 2011, VS-Theory 2010, FTfJP 2010

Recent papers

Subm.	Relaxed separation logic: a program logic for C11 concurrency (with Narayan)
ICFP'13	Mtac: a monad for typed tactic programming in Coq (with Ziliani, Dreyer, Krishaswami, Nanevski) [Project page]
CONCUR'13	Aspect-oriented linearizability proofs (with Henzinger, Sezgin)
Draft	Parametric bisimulations: a logical step forward (with Hur, Neis, Dreyer) [Technical appendix & Coq scripts]
ITP'13	Adjustable references [Project page]
TASE'13	A programming language approach to fault tolerance for fork-join parallelism (with Zengin)
POPL'13	The power of parameterization in coinductive proof (with Hur, Neis, Dreyer) [Project page]
Tech.rep.	The transitive composability of relation transition systems (with Hur, Neis, Dreyer) [Coq scripts]
JACM	CompCertTSO: a verified compiler for relaxed-memory concurrency (with Sevcik, Zappa Nardelli, Jagannathan, Sewell) [Project page]
POPL'12	The marriage of bisimulations and Kripke logical relations (with Hur, Dreyer, Neis) [Technical appendix] [Coq scripts]
SAS'11	Verifying fence elimination optimisations (with Zappa Nardelli) [Project page]
MFPS'11	Concurrent separation logic and operational semantics [More details & mechanized proofs]
LICS'11	Separation logic in the presence of garbage collection (with Hur, Dreyer) [Technical appendix]
POPL'11	Relaxed-memory concurrency and verified compilation (with Sevcik, Zappa Nardelli, Jagannathan, Sewell) [Project page]

 
[All publications...] [Pubs@DBLP] [Pubs@GoogleScholar]