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

MPI-SWS, Gottlieb-Daimler-Str. 49
D-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 postdoc 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.

New: 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 I have written the following software verification tools:

• SmallfootRG: a verification tool that proves safety properties of concurrent programs.
• Cave: a verification tool for proving linearizability of concurrent programs.

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

Recent papers

Subm.	The transitive composability of relation transition systems (with Hur, Neis, Dreyer) [Technical appendix] [Coq scripts]
Subm.	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 & Isabelle 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]
CAV'10	Automatically proving linearizability
ECOOP'10	Concurrent abstract predicates (with Dinsdale-Young, Dodds, Gardner, Parkinson)
POPL'10	Structuring the verification of heap-manipulating programs (with Nanevski, Berdine)
VMCAI'10	RGSep action inference

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