source: CIVL/README.md@ 9d0c04c

# CIVL: The Concurrency Intermediate Verification Language

v1.22

## 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, Pthread, CUDA, and Chapel. CIVL-C also
  provides a number of primitives supporting verification.
* 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.
* a number of translators from various commonly-used languages
  and APIs to CIVL-C. (This part is still a work in progress.)

CIVL is developed by the Verified Software Laboratory at the
University of Delaware Department of Computer Science.
For more information, visit <https://civl.dev>

**Active Developers:**

- Stephen F. Siegel
- Alexander Wilton

**Previous Developers:**

- John Edenhofner
- Andre Marianiello
- Michael Rogers
- Timothy K. Zirkel
- Manchun Zheng
- Yihao Yan
- Matthew B. Dwyer
- Mitchell Gerrard
- Wenhao Wu
- Ziqing Luo

## License

CIVL is open source software distributed under the GNU
General Public License.  However, the libraries used by CIVL
(and incorporated into the complete distribution) use various
licenses.  See directory licenses for the license of each component.

## Updates from v1.21

1. Upgraded to Java 17
2. Overhauled repository structure by moving ABC, SARL, and GMC
   repositories into this one.
3. Core language changes
    1. Only the first statement in an `$atomic` block is allowed to block.
    2. `$yield` can be used to release the lock of the atomic block
    3. Removed `$atom`
4. Total overhaul to OpenMP transformations. Now includes a robust data
   race detection feature as described in CAV 2023 paper 'Model Checking
   Race-freedom When "Sequential Consistency for Data-race-free Programs"
   is Guaranteed'
5. A large number of bug fixes and small improvements.

## Updates from v1.20

1. refine the Fortran extension for paper submitted to TACAS 2022
    1. Complete Fortran Array Descriptor for tracking changes made on
       index ranges by array section and reshape operations.
       Any declared array type is transformed into a Fortran array
       descriptor by Fortran to CIVL-C AST transformer.
    2. Introduce four basic CIVL verification primitives Fortran bindings
        1. Type qualifiers:
            - `!$CVL $input`:  indicates that all variables declared immediately
              in the next line are symbolic and read-only.
            - `!$CVL $output`: indicates that all variables declared immediately
              in the next line are write-only and used for
              verifying functional output equivalence.

           A type declaration statement is required to be used immediately
           after any CIVL type qualifier and variables qualified shall follow
           read/write constraints mentioned above.
           CIVL assumption primitives can be used for limiting the value range
           of variables qualified by `!$CVL $input`.
           e.g.,

           ```fortran
           !$CVL $input
           integer :: n, a(n)
           !! both 'n' and elements of 'a' are symbolic and read-only
           !$CVL $output
           integer :: sum
           !! sum is write-only and can be used for comparing with another
           !! program, which also has 'sum' with a same type and qualified
           !! by '!$CVL $output'
           ```

        2. Verification
            - `!$CVL $assume(logic_expr)`;
              Make CIVL only explores paths, whose path conditions shall
              make `logic_expr` to be true.
              Set the value range for varialbes qualified by `!$CVL $input`
            - `!$CVL $assert(logic_expr)`;
              Checks predicates representing specific correctness properties
              that users expect to verify.
              If any CIVL assertion primitive is evaluated as false, then
              CIVL shall report an assertion violation.
    3. Add supports for additional Fortran features include:
        1. `inout` and `out` attributes declared by `intent` statement
        2. compound types with fields having scalar types.
        3. pointer types to scalar types.
        4. logic expression evaluation without short-circuits
        5. line truncation for fixed and free forms
        6. other features are shown here:
           <https://vsl.cis.udel.edu/trac/civl/wiki/FortranTransformations>
    4. Add test cases imported from SMACK verification suite
       <https://github.com/soarlab/gandalv/>
2. CUDA Support Improvement
    1. Fixed CUDA bug in which CUDA kernel declarations were not being
       transformed properly
    2. Fixed source info bug (`completeSources` wasn't being called
       everywhere that it should)
    3. Fixed short circuit bug described in ticket #943
    4. Added small optimization to short circuit transformer to allow
       for finer granularity of its transformation
3. Other Improvement and Fixed Bugs
    1. `MPI_Comm` types can be compared by equality operator (`==`).
    2. Java-Doc improvements

## Updates from v1.19

1. added new language primitives:
    1. `$local_start()` and `$local_end()`
       An execution of the statements in between of this pair, including this pair themselves,
       is NOT ONLY uninterruptable BUT ALSO purely local to the view of the verifier.
    2. `$read_set_push()` and `$read_set_pop()` (the correspondence for write set has already been supported)
       This pair of primitives can be used to turn on/off the capturing of read set during execution.
2. added Fortran support for translating basic Fortran features into CIVL-AST
   (see: <https://vsl.cis.udel.edu/trac/civl/wiki/FortranTransformations>)
3. added simple Fortran verification examples (edited)

## Binary Installation

For most users, this will be the easiest way to install and
use CIVL.  Developers should instead follow the instructions for
"Source Installation" below.

1. Install at least one of the theorem provers below.
   The more provers you install, the more precise CIVL analysis will
   be.  Note that CIVL only requires the binary executable
   version of each prover; you can ignore the libraries, various
   API bindings, etc.   You just need to ensure that
   each binary executable is in your PATH when you run
   `civl config`.   The currently supported provers are:

    - CVC4,  <http://cvc4.cs.nyu.edu/downloads/>
    - Z3, <http://z3.codeplex.com/SourceControl/latest>

2. Install a Java 17 SDK if you have not already.  Go to

   <http://www.oracle.com/technetwork/java/javase/downloads/>

   for the latest from Oracle.  On linux, you can instead use
   the package manager:

   ```sh
   sudo apt install openjdk-17-jdk
   ```

3. Download the CIVL distribution from <http://vsl.cis.udel.edu/civl>.

4. Unzip and untar the CIVL distribution file if this
   does not happen automatically.  This should result in a
   folder named CIVL-TAG, where TAG is some version ID string.
   This folder contains the following:

    - README   : this file
    - bin      : containing one executable sh script called `civl`
    - lib      : containing civl-TAG.jar
    - doc      : containing the manual and the tutorial of CIVL
    - emacs    : CIVL-C emacs mode and its installation instructions
    - licenses : licenses for CIVL and included libraries
    - examples : some example CIVL programs

5. You can move the CIVL folder wherever you want.
   The JAR file in the lib directory is all you need to run CIVL.
   You may also move this jar file wherever you want.   You
   run CIVL by typing a command that begins
   `java -jar /path/to/civl-TAG.jar ...`.  For convenience
   you may instead use the shell script `civl` in bin,
   which allows you to replace `java -jar /path/to/civl-TAG.jar`
   with just `civl` on the command line.   Simply edit the `civl` script
   to reflect the path to `civl-TAG.jar` and place the script
   somewhere in your `PATH`.   Alternatively, you can just define
   an alias in your `.profile`, `.bash_profile`, or equivalent, such as

   ```sh
   alias civl='java -jar /path/to/civl-TAG.jar'
   ```

   In the following, we will assume that you have defined
   a command `civl` in one these ways.

6. Type `civl config`.  This should report that it found
   the theorem provers you installed (and are in your `PATH`).
   It should create a file called `.sarl` in your home directory
   which you can also edit by hand.

## Source Installation

Instructions found here:
<https://vsl.cis.udel.edu/trac/civl/wiki/Be%20a%20CIVL%20developer>