Title: Verification of Concurrent Programs with Civl

Speaker: Shaz Qadeer    (bio) (bio)

Shaz Qadeer is an ACM Fellow. His research focuses on practical tools for the construction of verified concurrent and distributed systems. He is currently employed as a software engineer in the Core Infrastructure department at Meta.

When: Tuesday, 11 July 2023 at 1900 hrs (IST)       

Abstract:
The Civl verifier introduces layered refinement, a new approach to the construction of verified concurrent programs and their proofs. This approach simplifies and scales (human and automated) reasoning by enabling a concurrent program to be represented and manipulated at multiple layers of abstraction. These abstraction layers are chained together via simple program transformations; each transformation is justified by a collection of automatically-checked verification conditions. Civl proofs are maintainable and reusable, specifically eliminating the need to write complex invariants on the low-level encoding of the concurrent program as a flat transition system. Civl has been used to construct verified low-level implementations of complex systems such as a concurrent garbage collector, a consensus protocol, and shared-memory data structures.