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 CIVL), but most users will want to use CIVL through the user interface (see 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: edu.udel.cis.vsl.civl.util.IF
   4. entry point: none
2. config
   1. responsibilities: static configurations of the system
   2. uses: gmc
   3. interface: edu.udel.cis.vsl.civl.config.IF
   4. entry point: CIVLConfiguration
3. transform
   1. responsibilities: transformations of an AST
   2. uses: config, abc, sarl
   3. interface: edu.udel.cis.vsl.civl.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: edu.udel.cis.vsl.civl.model.IF
   4. entry point: Models
   5. submodules
      1. expression
         1. responsibilities: definitions of various expressions of CIVL
         2. interface: edu.udel.cis.vsl.civl.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: edu.udel.cis.vsl.civl.model.IF.location
         3. entry point: none
      3. statement
         1. responsibilities: definitions of various statements of CIVL
         2. interface: edu.udel.cis.vsl.civl.model.IF.statement
         3. entry point: none
      4. type
         1. responsibilities: definitions of various types of CIVL
         2. interface: edu.udel.cis.vsl.civl.model.IF.type
         3. entry point: none
      5. variable
         1. responsibilities: definitions of a variable of CIVL
         2. interface: edu.udel.cis.vsl.civl.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: edu.udel.cis.vsl.civl.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: edu.udel.cis.vsl.civl.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: edu.udel.cis.vsl.civl.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: edu.udel.cis.vsl.civl.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: edu.udel.cis.vsl.civl.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: edu.udel.cis.vsl.civl.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: edu.udel.cis.vsl.civl.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: edu.udel.cis.vsl.civl.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: edu.udel.cis.vsl.civl.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: edu.udel.cis.vsl.civl
    4. entry point: CIVL

Packages

Package	Description
edu.udel.cis.vsl.civl	The main package for CIVL, providing a command line interface and a class "CIVL" that invokes all the components in the CIVL tool chain to perform requested tasks.
edu.udel.cis.vsl.civl.analysis.IF	Module analysis provides a list of analyzers for static/runtime analyzing of a program.
edu.udel.cis.vsl.civl.config.IF	Module config provides static configurations of the CIVL tool.
edu.udel.cis.vsl.civl.dynamic.IF	Module dynamic provides general computations of symbolic expressions, including the pretty printing method.
edu.udel.cis.vsl.civl.kripke.IF	Module kripke provides the definition of various transitions and the enabler and state manager of CIVL.
edu.udel.cis.vsl.civl.log.IF	Module log provides the data structure for logging errors during verification.
edu.udel.cis.vsl.civl.model.IF	Module model defines a static model, i.e., the control flow graph, representation of a CIVL-C program.
edu.udel.cis.vsl.civl.model.IF.contract
edu.udel.cis.vsl.civl.model.IF.expression	Submodule model.expression defines expression in CIVL.
edu.udel.cis.vsl.civl.model.IF.expression.reference
edu.udel.cis.vsl.civl.model.IF.location	Submodule model.location defines a location in the control flow graph of CIVL.
edu.udel.cis.vsl.civl.model.IF.statement	Submodule model.statement defines a statement of a CIVL-C program.
edu.udel.cis.vsl.civl.model.IF.type	Submodule model.type defines types in CIVL.
edu.udel.cis.vsl.civl.model.IF.variable	Submodule model.variable defines variables in CIVL.
edu.udel.cis.vsl.civl.predicate.IF	Module predicate defines predicates that are required to hold for any CIVL-C programs.
edu.udel.cis.vsl.civl.run.IF	Module run parses command line inputs and initializes the tool.
edu.udel.cis.vsl.civl.semantics.IF	Module semantics implements the semantics of CIVL-C.
edu.udel.cis.vsl.civl.slice.IF
edu.udel.cis.vsl.civl.state.IF	Module state is responsible for the creation and manipulation of states of a CIVL model.
edu.udel.cis.vsl.civl.transform.IF	Module transform defines various kinds of transformations of an AST into a CIVL AST.
edu.udel.cis.vsl.civl.util.IF	Module util provides various general-purpose utilities used by CIVL.