Research
I have completed my PhD in the
Cambridge Programming Research Group (CPRG)
being supervised by
Alan Mycroft
and Matthew Parkinson.
My research is about proving correctness of complex concurrent algorithms.
I have developed techniques for proving linearisability and a new logic,
RGSep, which combines rely-guarantee reasoning and separation logic.
I now work for Microsoft Research Cambridge
(my new home page).
Further information...
NEW: Public release of SmallfootRG 1.0
Publications
-
Modular safety checking for fine-grained concurrency.
Cristiano Calcagno, Matthew Parkinson, Viktor Vafeiadis.
In SAS 2007. LNCS, vol. 4634, pp. 233-238, Springer.
[pdf]
-
A marriage of rely/guarantee and separation logic.
Viktor Vafeiadis, Matthew Parkinson.
In CONCUR 2007. LNCS, vol. 4703, pp. 256-271, Springer.
[pdf]
-
Proving correctness of highly-concurrent linearisable objects.
Viktor Vafeiadis, Maurice Herlihy, Tony Hoare, Marc Shapiro.
In PPoPP 2006.
[pdf]
-
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.
[pdf]
All publications...
Contact Details
| Email: |
Viktor dot Vafeiadis at cl.cam.ac.uk |
| Address: |
William Gates Building
15 JJ Thomson Avenue
Cambridge
CB3 0FD
UK
|
| Tel: | +44 1223 763559 |
Supervisions
Part IB
Part II
