1. Overview
2. Description and examples
3. Download and installation
4. Documents
5. E-mail Lists
6. Developer Links
7. License

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, 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 concurrency languages/APIs to CIVL-C (currently, MPI, OpenMP, Pthreads, and CUDA).

The CIVL web application allows one to play CIVL through a web browser, without installing CIVL. Try it here.

See a more detailed description and examples of what CIVL does.

The CIVL developers are

• Matthew Dwyer, University of Nebraska
• Ziqing Luo, Verified Software Laboratory
• Michael Rogers, University of Nebraska
• Mitchell Gerrard, University of Nebraska
• Stephen Siegel, Verified Software Laboratory
• Manchun Zheng, Verified Software Laboratory
• Timothy Zirkel, Verified Software Laboratory
• Wenhao Wu, Verified Software Laboratory
• Yihao Yan Verified Software Laboratory

Its development is supported by the U.S. National Science Foundation grant CCF-0733035.

CIVL is open source software distributed under the GNU General Public License.

There is a related project in the University of Utah developing CIVL models of CUDA programs and the formal semantics of CIVL-C.

The CIVL platform should work on most Unix-like system. It is tested regularly on Linux and OS X. The source code can be obtained using Subversion, by checking out repository svn://vsl.cis.udel.edu/civl . Instructions for building from source are included. However, the pre-built distributions below are much easier to set up and get working. Each of the complete distributions includes all of the libraries used by CIVL, so you don't have to worry about installing them.

CIVL requires a Java 8 JVM. You can get one from Oracle here. You only need the JRE (runtime system) for using CIVL, but you can also install the complete JDK. On linux, you can alternatively sudo apt-get install openjdk-8-jdk .

• Latest stable release
• Latest unstable release
• Directory of all recent releases

1. The CIVL Manual: latest stable version
2. Publications
   • CIVL: The Concurrency Intermediate Verification Language
   • Using Symbolic Execution to Verify the Order of Accuracy of Numerical Approximations

1. CIVL Users: a list for users of CIVL, general discussion, problems, bug reports, etc. Open to all.
2. CIVL Developers: a list for the developers of CIVL.

1. Javadoc API
2. Trac site
3. JUnit Test Results (run after each commit)
4. Jacoco Coverage Report

CIVL is copyright 2013, 2014, 2015, Verified Software Laboratory, University of Delaware. CIVL is distributed under the terms of the GNU General Public License v3. See the directory licenses in the distribution for details.