The Civl verifier (https://civl-verifier.github.io/) 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.

The tutorial will present the technical context of the Civl verifier by discussing important classes of concurrent systems and surveying known methods for verification of such systems. This discussion will naturally motivate the presentation of the components of the proof methodology implemented in Civl. We will present yield invariants which is a compositional extension of Owicki-Gries, commutativity reasoning based on Lipton’s reduction, ownership constraints using linear types, and a method for establishing refinement between structured programs.