I am a post-doc researcher in the Programming Principles and Tools Group at Microsoft Research Cambridge. Before this, I was a PhD student at the University of Cambridge.
Research.
My research interests include program analysis/verification, programming languages, program logics and concurrency. In particular, I am interested in semi-automatically proving full functional correctness of concurrent imperative programs, especially of libraries of non-blocking and fine-grained concurrent algorithms. This involves establishing linearizability (refinement of a atomic sequential specification) and guaranteeing some forms of progress, such as lock-freedom. I have developped:
- RGSep: a program logic marrying rely/guarantee and separation logic; and
- SmallfootRG: a verification tool that proves safety properties of concurrent programs.
More recently, I have worked on making concurrent program verification more automatic and have co-developed deny-guarantee reasoning.
- Workshop on Verification of Concurrent Algorithms, Cambridge 1st-2nd May 2008
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.
Publications.
- RGSep action inference.
Viktor Vafeiadis.
To appear in VMCAI 2010. - Structuring the verification of heap-manipulating programs.
Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine.
Technical report MSR-TR-2009-104.
To appear in POPL 2010. - Bi-abductive resource invariant synthesis.
Cristiano Calcagno, Dino Distefano, Viktor Vafeiadis.
To appear in APLAS 2009. - Finding heap-bounds for hardware synthesis.
Byron Cook, Ashutosh Gupta, Stephen Magill, Andrey Rybalchenko, Jiri Simsa, Satnam Singh, Viktor Vafeiadis.
To appear in FMCAD 2009. - Deny-guarantee reasoning.
Mike Dodds, Xinuy Feng, Matthew Parkinson, Viktor Vafeiadis.
In ESOP 2009. Springer LNCS 5502, pp. 363-377. - Proving that nonblocking algorithms don't block.
Alexey Gotsman, Byron Cook, Matthew Parkinson, Viktor Vafeiadis.
In POPL 2009. ACM, pp. 16-28. - Shape-value abstraction for verifying linearizability.
Viktor Vafeiadis.
In VMCAI 2009. Springer LNCS, vol 5403, pp. 335-348. - Modular safety checking for fine-grained concurrency.
Cristiano Calcagno, Matthew Parkinson, Viktor Vafeiadis.
In SAS 2007. Springer LNCS, vol. 4634, pp. 233-238. - A marriage of rely/guarantee and separation logic.
Viktor Vafeiadis, Matthew Parkinson.
In CONCUR 2007. Springer LNCS, vol. 4703, pp. 256-271. - Proving correctness of highly-concurrent linearisable objects.
Viktor Vafeiadis, Maurice Herlihy, Tony Hoare, Marc Shapiro.
In PPoPP 2006. ACM. - Acute: high-level programming language design for distributed computation.
Peter Sewell, James J. Leifer, Keith Wansbrough, Francesco Zappa Nardelli, Mair Allen-Williams, Pierre Habouzit, Viktor Vafeiadis.
In ICFP 2005. ACM.
Contact details.
Address. Microsoft Research, 7 J J Thomson Avenue, Cambridge CB3 0FB, UK.
Email. viktorva [at] microsoft [dot] com
Telephone. +44 (0)1223 479 733
Fax. +44 (0)1223 479 999
