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, 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).

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

Publications

Talks