September 18, 2020
Abstract
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: https://civl-verifier.github.io/.
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 (https://github.com/libra/libra), and (2) CIVL, a reifier for concurrent programs (https://civl-verifier.github.io/). His research interests span all aspects of development of robust and secure software.