Civl is a verifier for concurrent programs following two core design principles.
-
Layered Refinement (instead of monolithic proofs): Programs are verified across multiple layers of stacked refinements. Each refinement layer corresponds to a simplifying program transformation. Proof construction becomes more productive by decomposing the problem into small, manageable, and automatable pieces. The resulting proofs become simpler and easier to reuse.
-
Structured Programs (instead of transition systems): Each layer of abstraction (from low-level implementations to high-level specifications) is represented in the same language of structured programs. This naturally bridges the verification gap down to implementations and enables the utilization of program structure in proofs. All layers (and their connection) are compactly expressed together as a single syntactic unit in a layered concurrent program.
Civl supports established verification techniques for concurrent programs, including stepwise-refinement, gated atomic actions, mover types, inductive invariants, noninterference reasoning, and linear permissions. It also incorporates newer verification techniques and methodologies, like yield invariants, inductive sequentialization, and synchronization.
Civl is built as a conservative extension of Boogie, a verifier for sequential programs. Civl decomposes proof checking into modular verification conditions that are automatically verified by a theorem prover/SMT solver.
Getting Started
Civl is implemented as part of Boogie, which can be installed from a NuGet package or built from source, and requires the Z3 theorem prover.
To verify a Civl program, simply invoke Boogie on the program as follows:
$ boogie Test/civl/ticket.bpl
Boogie program verifier finished with 8 verified, 0 errors
To inspect the plain Boogie program that Civl generates, use the option -civlDesugaredFile:<file.bpl>
.
Further available options are listed by -help
.
Resources
For a general overview, we have a tutorial (slides, recording).
For more detailed guidance about using Civl, we have documentation.
We recommend looking at simple
examples from our suite of samples,
like Program*.bpl
, cav2020-*.bpl
, and freund.bpl
.
Other notable examples include
a verified garbage collector,
lock implementations
(spinlock,
ticket,
seqlock),
concurrent data structures
(Treiber stack,
FastTrack vector clocks),
distributed protocols
(Paxos,
two-phase commit /
2PC,
Chang-Roberts),
and many more.
Publications
- The Civl Verifier
Bernhard Kragl, Shaz Qadeer
FMCAD 2021 - Refinement for Structured Concurrent Programs
Bernhard Kragl, Shaz Qadeer, Thomas A. Henzinger
CAV 2020 - Inductive Sequentialization of Asynchronous Programs
Bernhard Kragl, Constantin Enea, Thomas A. Henzinger, Suha Orhun Mutluergil, Shaz Qadeer
PLDI 2020 - Synchronizing the Asynchronous
Bernhard Kragl, Shaz Qadeer, Thomas A. Henzinger
CONCUR 2018 - Layered Concurrent Programs
Bernhard Kragl, Shaz Qadeer
CAV 2018 - Automated and Modular Refinement Reasoning for Concurrent Programs
Chris Hawblitzel, Erez Petrank, Shaz Qadeer, Serdar Tasiran
CAV 2015
Talks
- The Civl Verifier @ FMCAD 2021
- Reifying Concurrent Programs @ University of Paris VII
- Refinement for Structured Concurrent Programs @ CAV 2020
- Civl-ized Concurrent Programs @ DSV 2020
- Inductive Sequentialization of Asynchronous Programs @ PLDI 2020
Team
If you are interested in Civl, please get in touch!