Title: Rely/Guarantee-thinking and Separation Logic
Presenters: Viktor Vafeiadis and Cliff Jones
Duration: half day
When: Tuesday morning, 21 June 2011

Reasoning about concurrent programs has long been recognized as challenging. Early approaches often tried to identify useful cases where the messy problems caused by interference could be avoided - essentially the attempt was to show that "races" could not occur. Recently, Separation Logics have provided very convenient ways of reasoning about such situations and clever notations have made proofs about even intricate low-level code quite tractable. A different challenge is reasoning about "racey" programs. Approaches like rely/guarantee reasoning face interference head on and include assertions about permissible interference. Although some people would regard this as masochism, it transpires that accepting interference at abstract levels of design can result in some clear developments of even race-free programs. RGSep has already shown that unification of rely/guarantee thinking and separation logic offers a powerful new tool. We will try to indicate clearly the strengths of the two approaches and indicate more ways of combining these strengths.

Viktor Vafeiadis is a researcher at the Max Planck Institute for Software Systems (MPI-SWS) specialising in the verification of concurrent programs, and is one of the developers of RGSep, a program logic that combines rely/guarantee reasoning with separation logic. Viktor received his Ph.D. in 2008 from the University of Cambridge and, prior to joining MPI-SWS, has held post-doctoral research positions at Microsoft Research and at the University of Cambridge.

His research contributions include inventing new concurrent program logics (RGSep and deny/guarantee); developing automated verification tools (SmallfootRG and Cave) for proving correctness properties of concurrent algorithms; and verifying some particularly challenging algorithms manually (e.g., mcas), mechanically (e.g., fast congruence closure), or automatically (e.g., lazy set). Currently, he is also working on verified compilation for concurrent programming languages.

Cliff Jones is currently Professor of Computing Science at Newcastle University (he is also FREng and FACM). He is a long-standing member of the Formal Methods community having been one of the original developers of VDM. Of most relevance to this tutorial, he originated much of the VDM material relating to program specification and design as well as the rely/guarantee approach to specifying and reasoning about concurrency. He has also been involved in the development and use of several generations of support tools for formal methods.