Colloquium - Reifying Concurrent Programs

April 2, 2021 - 4:00pm
Zoom - See emails for details
Shaz Qadeer
Novi | Facebook

Program reification is 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. Program reification makes proofs 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.

I will present Civl, a reifier for concurrent programs. Civl has been used to construct verified low-level implementations of complex systems such as a concurrent garbage collector, consensus protocol, and shared-memory data structures. Civl is publicly available:

This work has been done jointly with Bernhard Kragl (IST Austria).


Shaz QadeerShaz Qadeer works at Novi, a group at Facebook aiming to build large-scale financial services. He is currently working on two projects: (1) Move, the programmable piece of the Diem blockchain (, and (2) Civl, a reifier for concurrent programs ( His research interests span all aspects of development of robust and secure distributed systems.