Colloquium - Reifying Concurrent Programs

Date: 
April 2, 2021 - 4:00pm
Location: 
Zoom - See emails for details
Speaker: 
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: civl-verifier.github.io.

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

Bio

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 (github.com/diem), and (2) Civl, a reifier for concurrent programs (civl-verifier.github.io). His research interests span all aspects of development of robust and secure distributed systems.