= CIVL: The Concurrency Intermediate Verification Language =

== About ==
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).

== Downloads ==

* [http://vsl.cis.udel.edu/lib/sw/civl/current/latest/ Latest stable release]
* [http://vsl.cis.udel.edu/lib/sw/civl/trunk/latest/ Latest unstable release]
* [http://vsl.cis.udel.edu/lib/sw/civl/ Older releases]
* [http://civl.cis.udel.edu/app/ CIVL Web App]

== Examples & Case Studies ==

* [wiki:Tour A Brief Tour of CIVL with Examples]
* [https://dl.acm.org/citation.cfm?id=3090070 CIVL Solutions to VerifyThis 2016 Challenges]
* [https://dl.acm.org/citation.cfm?id=3145488 Towards Self-Verification in Finite Difference Code Generation]
* [https://link.springer.com/chapter/10.1007/978-3-319-99725-4_14 Verifying Properties of Differentiable Programs] 

== Documents & Publications ==

* [https://vsl.cis.udel.edu/lib/sw/civl/civl-manual.pdf  CIVL Manual]
* [https://vsl.cis.udel.edu/pubs/civl_sc_2015.html CIVL: The Concurrency Intermediate Verification Language]
* [https://vsl.cis.udel.edu/pubs/civl_eurompi_2017.html  Verification of MPI programs using CIVL]
* [https://science.energy.gov/~/media/ascr/pdf/programdocuments/docs/2017/HPC_Correctness_Report.pdf DOE Report of the HPC Correctness Summit]
* [https://vsl.cis.udel.edu/pubs/civl_verifythis_2016.html CIVL Solutions to VerifyThis 2016 Challenges]
* [https://vsl.cis.udel.edu/pubs/civl_svcomp_2016.html CIVL: Applying a General Concurrency Verification Framework to C/Pthreads Programs Competition Contribution]
* [https://vsl.cis.udel.edu/pubs/civl_ase_2015.html CIVL: Formal Verification of Parallel Programs]
* [https://vsl.cis.udel.edu/pubs/civl_tr_2014.html Tech Report: CIVL: The Concurrency Intermediate Verification Language]
* [https://vsl.cis.udel.edu/pubs/index.html VSL Publication List]

== How to Cite CIVL ==
{{{
@Inproceedings{siegel-etal:2015:civl_sc,
  author = {Stephen F.\ Siegel and Manchun Zheng and Ziqing Luo and
            Timothy K.\ Zirkel and Andre V.\ Marianiello and John G.\ Edenhofner
            and Matthew B.\ Dwyer and Michael S.\ Rogers},
  title = {{CIVL}: The Concurrency Intermediate Verification Language},
  booktitle = {SC15: International Conference for High Performance
               Computing, Networking, Storage and Analysis, Proceedings},
  series = {SC '15},
  year = {2015},
  month = {Nov},
  publisher = {IEEE Press},
  address = {Piscataway, NJ, USA},
  pages = {61:1-61:12}
}
}}}

== Bug Reports ==
To report a bug in CIVL, send an email to `civl-dev` at `googlegroups`  dot `com`.
Include as many details as possible, such as the CIVL command, source files (these may be attached), the CIVL version, 
and the output, including any error message.

== Developers ==
* Current Developers: Ziqing Luo, [https://vsl.cis.udel.edu/siegel.html Stephen F. Siegel] and Wenhao Wu
* Other Contributors: Matthew Dwyer, John Edenhofner, Mitchell Gerrard, Andre Marianiello, Michael Rogers, Yihao Yan, Manchun Zheng and Timothy Zirkel.

[wiki:DeveloperPage]