Scaling Verification of Concurrent Programs with the Civl Verifier
Explore the Civl verifier and its innovative layered refinement approach for verifying concurrent programs in this 3.5-hour tutorial. Learn how to simplify and scale reasoning by representing programs at multiple abstraction layers, chained together through simple transformations. Discover how Civl proofs enhance maintainability and reusability, eliminating the need for complex invariants on low-level encodings. Examine real-world applications of Civl in verifying complex systems like concurrent garbage collectors, consensus protocols, and shared-memory data structures. Delve into the technical context of Civl, discussing various concurrent systems and surveying verification methods. Gain insights into key components of Civl's proof methodology, including yield invariants, commutativity reasoning, ownership constraints using linear types, and methods for establishing refinement between structured programs.