Viktor Vafeiadis

Publications

Journals

• 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. To appear in Journal of Functional Programming. [PDF]

Conference proceedings

• A marriage of rely/guarantee and separation logic.
  Viktor Vafeiadis, Matthew Parkinson.
  In CONCUR 2007. LNCS, vol. 4703, pp. 256-271, Springer.
  [PDF]
• Modular safety checking for fine-grained concurrency.
  Cristiano Calcagno, Matthew Parkinson, Viktor Vafeiadis.
  In SAS 2007 (Static Analysis Symposium). LNCS, vol. 4634, pp. 233-238, Springer.
  [PDF]
• Proving correctness of highly-concurrent linearisable objects.
  Viktor Vafeiadis, Maurice Herlihy, Tony Hoare, Marc Shapiro.
  In Proceedings of Principles and Practices of Parallel Programming (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 Proceedings of the International Conference of Functional Programming (ICFP 2005).
  [PDF]

Technical reports

• A marriage of rely/guarantee and separation logic.
  Viktor Vafeiadis and Matthew Parkinson.
  Technical report UCAM-CL-TR-687. University of Cambridge Computer Laboratory, June 2007.
  [PDF]
• A safety proof of a lazy concurrent list-based set implementation.
  Viktor Vafeiadis, Maurice Herlihy, Tony Hoare, and Marc Shapiro.
  Technical report UCAM-CL-TR-659. University of Cambridge Computer Laboratory, January 2006.
  [PDF]

Drafts

• Proving linearisability of lock-free algorithms. Viktor Vafeiadis.
  Draft, April 2006. Revised, February 2007.
  [PDF]

Internal reports

• Thesis proposal. Viktor Vafeiadis. July 2005. [PDF]
• First year report. Viktor Vafeiadis. July 2005. [PDF]
• A compiler for Standard ML. Viktor Vafeiadis. Part II project report. May 2004.

Slides

• Rely/guarantee meets separation logic. Semantics Lunch. November 2006. [PDF]
• Rely/guarantee meets separation logic. Concurrency Meeting. October 2006. [PDF]
• A rely/guarantee proof of a non-blocking stack algorithm. CPRG seminar. June 2006. [PDF]
• Proving correctness of highly-concurrent linearisable objects. PPoPP. March 2006. [PDF]
• Proof techniques for fine-grain concurrency. CPRG seminar. November 2005. [PDF]
• Introduction to the verification of concurrent programs. CPRG seminar. August 2005. [PDF]

Return to main page...