CIVL: Concurrency Intermediate Verification Language

Overview

CIVL is a framework encompassing ...

• a programming language, CIVL-C, which adds to C a number of concurrency primitives, as well as the ability to define functions in any scope. Together, these features make for a very expressive concurrent language that can faithfully represent programs using various APIs and parallel languages, such as MPI, OpenMP, CUDA, and Chapel. CIVL-C also provides a number of primitives supporting verification.
• a number of transformers from various commonly-used concurrency languages/APIs to CIVL-C (currently, MPI, OpenMP, Pthreads, and CUDA).
• a model checker which uses symbolic execution to verify a number of safety properties of CIVL-C programs. The model checker can also be used to verify that two CIVL-C programs are functionally equivalent.

Download

There are several options for downloading CIVL: stable release and unstable nightly releases.
The current stable version is version 1.5.

• latest stable release (recommended): v1.5
• latest unstable release: here
• previous stable and unstable releases: here

Demonstration

• watch the video demonstrating using CIVL to verify an OpenMP+MPI hybrid program that calculates the value of π;
• play the virtual machine containing a working demonstration of CIVL following the instructions here;
• experiment archive demonstrating CIVL using two scenarios, containing the CIVL tool, example source and instructions for verifying the examples as described by the two scenarios;
• use the CIVL web application that allows one to play CIVL through a web browser, without installing CIVL.

Documentation

• CIVL manual: latest stable version
• Technical report: CIVL: The Concurrency Intermediate Verification Language

Development

• Quick references for CIVL developers: Java Documentation of CIVL APIs    latest stable   latest unstable
• Bug reporting system: CIVL Trac
• Automatic tests:
  • Junit tests: latest stable   latest unstable
  • Code coverage report: latest stable tests   latest unstable tests
• Related projects: ABC SARL

Screenshots

CIVL is a command-line based tool. It provides five commands: show, run, verify, compare and replay. The usage of these commands is explained as the following, which displays the output provided by "civl help". Moreover, there a number of options to be configured, e.g., showTransitions for printing transitions.

• civl help
  
• civl verify: the following figures demonstrate verifying a CIVL-C implementation of the dining philosopher problem. The option "-inputB=4" specifies the value for the input variable for the upper bound of the number of philosophers in the program, whereas the option "-min" requests the model checker to search for a minimal counterexample.
  
• civl replay: replays the mininal counterexample produced by the above civl verify command.