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, yield invariants, linear permissions, 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).

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, Chang-Roberts), and many more.

Publications

Talks

This site uses Just the Docs, a documentation theme for Jekyll.