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