Motivation Concurrency verification is challenging! Exponential state space caused by interleaving of execution. Memory aliasing makes it harder to ensure non-interference. Modularity is the key!Motivation Concurrency verification is challenging! T1 T1 T1 T2 T2 T2 Exponential state space caused by interleaving of execution. Memory aliasing makes it harder to ensure non-interference. Modularity is the key!