Proof methods for concurrent programs

Lectures given at the Master Parisien de Recherche en Informatique, 2010.

Part of the Concurrency course, in collaboration with Frank Valencia, James Leifer, Emmanuel Haucourt.

  1. Slides on shared memory, Hoare logic, and separation logic.
  2. Slides on concurrent separation logic.
  3. Slides on Owicki-Gries and Rely/Guarantee.
  4. Introduction to relaxed memory models (no slides, but a reference).

Some exercises.

The exam questions.

References: If you want more:

NEW: Francesco Zappa Nardelli proposes two stages for 2010/2011:

  1. verified compilation of C / C++ low-level atomics to x86, Power or ARM multiprocessors;
  2. relaxed memory concurrency and compiler optimisations.

Email: Francesco.Zappa_Nardelli (at)

Address: Francesco Zappa Nardelli, Projet Moscova, INRIA Paris-Rocquencourt, Domaine de Voluceau, B.P. 105, 78153 Le Chesnay Cedex, France

Last updated:  .