Shaz Qadeer
September 18, 2020


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.

We have designed and implemented 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).

About Shaz Qadeer

Shaz 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 Libra blockchain (, and (2) CIVL, a reifier for concurrent programs ( His research interests span all aspects of development of robust and secure software.