Viktor Vafeiadis

Publications

Conference proceedings

• 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 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

• Modular safety checking for fine-grain concurrency. Cristiano Calcagno, Matthew Parkinson, and Viktor Vafeiadis.
  Submitted to CAV, January 2007.
  
• A marriage of rely/guarantee and separation logic. Viktor Vafeiadis and Matthew Parkinson.
  Submitted to LICS, January 2007.
  [PDF]
• 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...