Semantics and tools for low-level concurrent programming

ER02 research school, January 14-18, 2013, ENS Lyon, France.

Lecturers: Mark Batty, Alastair Donaldson, Martin Vechev, Francesco Zappa Nardelli.


  • Slides on hardware models (Zappa).
  • Slides on x86-TSO (Batty).
  •    Exercices on x86-TSO.
  • Slides on ARM/Power (Batty/Zappa).
  • Slides on programming language models (Zappa).
  •    Exercices on ARM/Power and on the DRF model.
  • Slides on C11/C++11 (Batty).
  • Slides on machine-assisted concurrent programming (part 1) (Vechev).
  •    Exercices on C11/C++11.
  •    Exercices on machine-assisted concurrent programming.
  • Slides on machine-assisted concurrent programming (part 2) (Vechev).
  • Slides on verification techniques for GPUs (part 1) (Donaldson).
  • Slides on verification techniques for GPUs (part 2) (Donaldson).
  •    Exercices on verification techniques for GPUs.

Email: Francesco.Zappa_Nardelli (at) inria.fr


Last updated:  .