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 (under construction)

We also recommend looking at simple examples from our test suite, like Program*.bpl, cav2020-*.bpl, and freund.bpl.

Publications

• 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

• Refinement for Structured Concurrent Programs @ CAV 2020
• Civl-ized Concurrent Programs @ DSV 2020
• Inductive Sequentialization of Asynchronous Programs @ PLDI 2020

Team

• Bernhard Kragl (IST Austria)
• Shaz Qadeer (Novi)

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