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