Constantin Enea and Shaz Qadeer will present a tutorial on the Civl verifier <https://popl24.sigplan.org/details/POPL-2024-tutorialfest/1/Scaling-Verification-of-Concurrent-Programs-with-the-Civl-Verifier> at POPL 2024 on Sunday January 14, 2024. If you are interested in automated and scalable reasoning about concurrent systems, you will find Civl of interest! A brief description of the tutorial contents is included below. ============================== Objectives: The tutorial aims to introduce the functionality of the Civl verifier, discuss its applicability and limitations, and a comparison with the state of the art. We will start with a description of practically important programming models that exhibit concurrency and require attention from verification researchers. Next, we will present an overview of trends in methods and tools for static verification of concurrent systems. Finally, we will present the different components and proof tactics implemented in Civl using illustrative examples and case studies. Topics to be covered: The tutorial will be structured in several sections that address the objectives mentioned above. 1. Classes of concurrent systems whose construction deserve reasoning support: - concurrent tasks operating on shared-memory (locks, non-blocking algorithms, weak memory, GPU programs) - processes communicating via channels, RPCs (distributed systems) - hardware controllers (memory controllers, pipelined processors), mixed hardware-software controllers (embedded systems) 2. Overview of trends in static concurrency reasoning: - Powering up program logics: extensions of Floyd-Hoare such as Owicki-Gries, Rely-Guarantee, Concurrent Separation Logic, etc. - The approach in Civl: amplifying simple program logics via orthogonal methods such as commutativity, linear types, refinement - Proof discovery: heuristic automation of proofs atop a particular proof system (much like the automation of type inference atop type checking) 3. Programming model of Civl: structured programs with possibly parallel and asynchronous procedure calls 4. Verification in Civl: - Yield invariants: noninterference reasoning that is as precise as Owicki-Gries and as compositional as rely-guarantee - Mover types: reduce interference using verification conditions for checking commutativity of atomic actions and a type system based on Lipton’s reduction - Ownership: disjoint distribution of resources ensured via linear types and verification conditions 5. Layered refinement in Civl: - Lifting refinement over transition systems to refinement over structured programs - A refinement chain of structured programs expressed as a single layered program - Each link in the refinement chain justified by a simulation proof supported by verification methods noted in #4 Presentation approach: The presentation will be driven by examples to illustrate challenges, explanation of core methods accessible to non-experts, and tool demonstration. Target audience: Researchers interested in concurrent systems, program analysis, and program verification Prerequisite knowledge: Logic, invariants, verification conditions, program analysis