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 the user interface (see {@link edu.udel.cis.vsl.civl.run.IF.UserInterface UserInterface}). 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
  2. transform
    1. responsibilities: transformations of an AST
    2. uses: abc
    3. interface: {@link edu.udel.cis.vsl.civl.transform.IF}
    4. entry point: CIVLTransform
  3. run
    1. responsibilities: parsing command line inputs and initial configurations of the tool
    2. uses: transform, abc
    3. interface: {@link edu.udel.cis.vsl.civl.run.IF}
    4. entry point: UserInterface
    4. TBC.