Civl is a verifier for concurrent programs following two core design principles.

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

Talks

Team

If you are interested in Civl, please get in touch!