= Contents =

* [#intro Introduction]
* [#lang Language]
* [#semantics Semantics]
* [#tools Tools]

= Introduction = #intro

== What is CIVL? ==

CIVL stands for ''Concurrency Intermediate Verification Language''.  The CIVL platform encompasses:

1. the programming language CIVL-C, a dialect of C with additional primitives supporting concurrency, specification, and modeling;
1. verification and analysis tools, including a symbolic execution-based model checker for checking various properties of, or finding defects in, CIVL-C programs; and
1. tools that translate from many commonly used languages/APIs to CIVL-C.

The CIVL-C language is primarily intended to be an intermediate representation for verification. A C program using MPI, CUDA, OpenMP, Pthreads, or another API (or even some combination of APIs), will be automatically translated into CIVL-C and then verified. The advantages of such a framework are clear: the developer of a new verification technique could implement it for CIVL-C and then immediately see its impact across a broad range of concurrent programs. Likewise, when a new concurrency API is introduced, one only needs to implement a translator from it to CIVL-C in order to reap the benefits of all the verification tools in the platform. Programmers would have a valuable verification and debugging tool, while API designers could use CIVL as a "sandbox" to investigate possible API modifications, additions, and interactions.

This manual covers all aspects of the CIVL framework, and is organized in parts as follows:

1. this introduction, including "quick start" instructions for downloading and installing CIVL and several examples;
1. a complete description of the CIVL-C language;
1. a formal semantics for the language; and
1. a description of the tools in the framework.

== Installation and Quick Start ==

== Examples ==

== Verifying  Programs ==

=== Verifying C Programs ===

=== Verifying C/MPI Programs ===

=== Verifying C/OpenMP Programs ===

=== Verifying CUDA-C Programs ===

=== Verifying C/Pthreads Programs ===

=== Verifying Fortran Programs ===

(under development)



= Language = #lang


= Semantics = #semantics


= Tools = #tools