Welcome to CIVL, the Concurrency Intermediate Verification Language tool. CIVL is a Java project for verifying concurrent programs written in CIVL-C, which is a C dialect with extensions to concurrent language constructs. The CIVL project uses ABC, SARL and GMC. The CIVL tool can be used to perform a number of tasks, including the following:

  1. preprocess or pass a CIVL-C program;
  2. verify a CIVL-C program;
  3. run a CIVL-C program;
  4. replay traces for a program.
In addition, it provides a framework for developing your own libraries or transformations on ASTs of various language extensions and libraries.

There is a simple command-line interface for CIVL (see {@link edu.udel.cis.vsl.civl.CIVL CIVL}), but most users will want to use CIVL through its API. To use the API, it is helpful to have some understanding of the modular structure of CIVL. The CIVL source code is decomposed into modules, each with a well-defined interface and set of responsibilities. Some of these modules are decomposed further into sub-modules. The top-level modules are:
  1. util
    1. responsibilities: simple general-purpose utility classes that do not use other parts of CIVL
    2. uses: nothing
    3. interface: {@link edu.udel.cis.vsl.civl.util.IF}
    4. entry point: none