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 refinement, where each refinement step corresponds to a small 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 (à la Lipton’s reduction), inductive invariants (noninterference reasoning à la Owicki-Gries and rely-guarantee), and linear permissions. It also incorporates newer verification techniques and methodologies, like yield invariants, inductive sequentialization, and synchronization.
Under the hood, Civl is built on top 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 directly 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 automatically detects Civl programs and internally sets the options
-useArrayTheory -lib -monomorphize
):
$ boogie Test/civl/ticket.bpl
Boogie program verifier finished with 19 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
Examples
Civl comes with an extensive test suite of example programs, including a verified garbage collector, the VerifiedFT dynamic race detector, lock implementations (spinlock, ticket, seqlock), concurrent data structures (treiber stack, work stealing queue), distributed protocols (Paxos, two-phase commit / 2PC, Chang-Roberts), and many more.
Documentation
We have a tutorial to help users get started with Civl.
We also recommend looking at simple
examples from our test suite,
like Program*.bpl
, cav2020-*.bpl
, and freund.bpl
.
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!