Separation is all you need: Foundations for Modular Verification

This lecture by the instructor covers the foundations for modular verification of realistic concurrent programs using Separation Logic. It discusses the challenges of concurrency, the importance of achieving thread-locality by keeping threads separated, and the application of Separation Logic to achieve this goal. The lecture also explores the weak spots of Separation Logic, the success story of Separation Logic in verification tools, and the complexities of shared mutable state in concurrent programs. It delves into the intricacies of reference counting, ghost permissions, and the formal verification of microkernel IPC. The lecture concludes with a discussion on the Rust programming language, its type system, and the challenges of ensuring safety in Rust programs.