Viktor Vafeiadis

I am a research associate at the University of Cambridge Computer Laboratory, where I did my undergraduate and postgraduate studies. Previously, I was a postdoc researcher at Microsoft Research Cambridge.

My research interests are: program analysis/verification, programming languages, program logics and concurrency.

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.

Software

I have written the following software tools:

• SmallfootRG: a verification tool that proves safety properties of concurrent programs. [More information...]
• Cave: a verification tool that proves linearizability of concurrent programs. (Please contact me for more information.)

Recent publications

CAV 2010	Automatically proving linearizability.
ECOOP 2010	Concurrent abstract predicates. (with Dinsdale-Young, Dodds, Gardner, Parkinson)
VMCAI 2010	RGSep action inference.
POPL 2010	Structuring the verification of heap-manipulating programs. (with Nanevski, Berdine)
APLAS 2009	Bi-abductive resource invariant synthesis. (with Calcagno, Distefano)
FMCAD 2009	Finding heap-bounds for hardware synthesis. (with Cook, Gupta, Magill, Rybalchenko, Simsa, Singh)
ESOP 2009	Deny-guarantee reasoning. (with Dodds, Feng, Parkinson)
POPL 2009	Proving that nonblocking algorithms don't block. (with Gotsman, Cook, Parkinson)
VMCAI 2009	Shape-value abstraction for verifying linearizability.
SAS 2007	Modular safety checking for fine-grained concurrency. (with Calcagno, Parkinson)
CONCUR 2007	A marriage of rely/guarantee and separation logic. (with Parkinson)

[All publications...]

PhD dissertation

• Modular fine-grained concurrency verification. Viktor Vafeiadis. University of Cambridge, July 2007.
  Also published as technical report UCAM-CL-TR-726, University of Cambridge Computer Laboratory, July 2008.

Contact Details

Email:	Viktor dot Vafeiadis at cl.cam.ac.uk
Address:	William Gates Building 15 JJ Thomson Avenue Cambridge CB3 0FD UK