CIVL: The Concurrency Intermediate Verification Language
                               v1.5

------------------------------ 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 http://vsl.cis.udel.edu/civl

Developers:

Matthew B. Dwyer
John Edenhofner
Mitchell Gerrard
Ziqing Luo
Andre Marianiello
Michael Rogers
Stephen F. Siegel
Manchun Zheng
Timothy K. Zirkel

------------------------------- 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.