Alexander Malkis, Researcher, IMDEA Software Institute
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