Introduces Iris, a logical framework for reasoning about safety and correctness of concurrent higher-order imperative programs, emphasizing its unique characteristics and applications.
Explores the foundations of modular verification using Separation Logic for realistic concurrent programs and discusses the challenges of shared mutable state in concurrency.
