Tutorial rehearsal: Verification of Multithreaded Programs

December 1, 2010

Alexander Malkis


Tutorial rehearsal: Verification of Multithreaded Programs

Time:   11:00am
Location:   Meeting room 302 (Mountain View), level 3

Contents: We give a short survey on the following topics on verification of multithreaded programs:

  • SPIN

  • Specification in Promela

  • Saving space: COLLAPSE & automata encoding

  • Saving time: partial order reduction

  • Modular verification for general programs

  • Owicki-Gries

  • Rely-guarantee

  • Thread-modular model checking

  • Multithreaded Cartesian abstraction

  • Concurrent procedures specification

  • Thread simpolfication

  • Cartesian abstraction refinement

  • Modular verification for resources & locks

  • Owicki-Gries

  • Concurrent separation logic