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 dev.civl.mc.CIVL CIVL}), but most users will want to use CIVL through the user interface (see {@link dev.civl.mc.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 dev.civl.mc.util.IF}
    4. entry point: none
  2. config
    1. responsibilities: static configurations of the system
    2. uses: gmc
    3. interface: {@link dev.civl.mc.config.IF}
    4. entry point: CIVLConfiguration
  3. transform
    1. responsibilities: transformations of an AST
    2. uses: config, abc, sarl
    3. interface: {@link dev.civl.mc.transform.IF}
    4. entry point: CIVLTransform
  4. model
    1. responsibilities: definitions of the control flow graph representation of a CIVL-C program
    2. uses: util, config, abc, gmc, sarl
    3. interface: {@link dev.civl.mc.model.IF}
    4. entry point: Models
    5. submodules
      1. expression
        1. responsibilities: definitions of various expressions of CIVL
        2. interface: {@link dev.civl.mc.model.IF.expression}
        3. entry point: none
      2. location
        1. responsibilities: definitions a location in the control flow graph of a CIVL-C program
        2. interface: {@link dev.civl.mc.model.IF.location}
        3. entry point: none
      3. statement
        1. responsibilities: definitions of various statements of CIVL
        2. interface: {@link dev.civl.mc.model.IF.statement}
        3. entry point: none
      4. type
        1. responsibilities: definitions of various types of CIVL
        2. interface: {@link dev.civl.mc.model.IF.type}
        3. entry point: none
      5. variable
        1. responsibilities: definitions of a variable of CIVL
        2. interface: {@link dev.civl.mc.model.IF.variable}
        3. entry point: none
  5. state
    1. responsibilities: creation and manipulation of states of a CIVL model.
    2. uses: config, model, gmc, sarl
    3. interface: {@link dev.civl.mc.state.IF}
    4. entry point: States
  6. log
    1. responsibilities: data structures for logging errors during verification.
    2. uses: model, state, gmc, sarl
    3. interface: {@link dev.civl.mc.log.IF}
    4. entry point: none
  7. dynamic
    1. responsibilities: general computations of symbolic expressions, including the pretty printing method.
    2. uses: util,model, state, log, sarl
    3. interface: {@link dev.civl.mc.dynamic.IF}
    4. entry point: Dynamics
  8. semantics
    1. responsibilities: implementation of the semantics of CIVL-C.
    2. uses: util, config, model, state, log, dynamic, sarl
    3. interface: {@link dev.civl.mc.semantics.IF}
    4. entry point: Semantics
  9. kripke
    1. responsibilities: implementation of the semantics of CIVL-C.
    2. uses: util, config, model, state, log, dynamic, semantics, gmc, sarl
    3. interface: {@link dev.civl.mc.kripke.IF}
    4. entry point: Kripkes
  10. predicate
    1. responsibilities: definitions of predicates that are required to hold for any CIVL-C programs.
    2. uses: model, state, log, dynamic, semantics, kripke, gmc, sarl
    3. interface: {@link dev.civl.mc.predicate.IF}
    4. entry point: none
  11. gui
    1. responsibilities: graphical interfaces for viewing counterexample traces.
    2. uses: model, state, dynamic, kripke, gmc, sarl
    3. interface: {@link dev.civl.mc.gui.IF}
    4. entry point: none
  12. library
    1. responsibilities: base implementation of libraries.
    2. uses: model, state, log, dynamic, semantics, kripke, sarl
    3. interface: {@link dev.civl.mc.library.IF}
    4. entry point: none
  13. run
    1. responsibilities: parsing command line inputs and initial configurations of the tool.
    2. uses: kripke, model, state, transform, util, abc, gmc, sarl
    3. interface: {@link dev.civl.mc.run.IF}
    4. entry point: UserInterface
  14. main
    1. responsibilities: parsing command line inputs and initial configurations of the tool
    2. uses: run
    3. interface: {@link dev.civl.mc}
    4. entry point: CIVL