IMDEA Software

Iniciativa IMDEA

Inicio > Eventos > Software Seminar Series > 2010 > Tutorial rehearsal: Verification of Multithreaded Programs
Esta página aún no ha sido traducida. A continuación se muestra la página en inglés.

Alexander Malkis

miércoles 1 de diciembre de 2010

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

Alexander Malkis, Researcher, IMDEA Software Institute

Tutorial rehearsal: Verification of Multithreaded Programs

Abstract:

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