Concurrency Semantics and Verification

This lecture covers the semantics and verification of concurrent programs, focusing on recursive functions in relational semantics, loops as a special case, and the need to model interleaving in concurrency. It also discusses difficulties in semantics, verifying an interpreter for a concurrent program, and running an interpreter on a schedule. The lecture concludes with the concept of running an interpreter on a schedule and the challenges of verifying concurrent programs.