Proof methods for concurrent programs

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

Part of the Concurrency course, in collaboration with Frank Valencia, Roberto Amadio, Emmanuel Haucourt.

  1. Shared memory, Hoare logic, and separation logic.
  2. Concurrent separation logic.
  3. Owicki-Gries and Rely/Guarantee.
  4. Relaxed memory models.
Up-to date slides available from the 2010 course web-page.

Some exercises.

The exam questions, and the solution.

References: If you want more:

Francesco Zappa Nardelli proposes two stages for 2009/2010:

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: