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 (à 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 also recommend looking at simple examples from our test suite, like Program*.bpl, cav2020-*.bpl, and freund.bpl.

Publications

Talks

Team

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