= 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 & Links ==

* [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]
* [wiki:Challenge A Challenge Exercise for Twente]
* [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] 

== CIVL Manual ==
* [wiki:"CIVL Manual: Introduction"]
* [wiki:"CIVL Manual: Language Reference"] (coming soon)
* [wiki:"CIVL Manual: Command Line Interface"] (coming soon)

== Documents & Publications ==

* [https://vsl.cis.udel.edu/pubs/isola18.html Symbolic Execution and Deductive Verification Approaches to VerifyThis 2017 Challenges], Ziqing Luo and Stephen F. Siegel, ISoLA'18.
* [https://vsl.cis.udel.edu/pubs/math_properties_sas18.html Verifying Properties of Differentiable Programs], J. Hückelheim, Z. Luo, S.H.K. Narayanan, S.F. Siegel, and P.D. Hovland, SAS'18.
* [https://vsl.cis.udel.edu/pubs/correctness_2017_towards.html Towards Self-Verification in Finite Difference Code Generation], J. Hückelheim, Z. Luo, F. Luporini, N. Kukreja, M. Lange, G. Gorman, S.F. Siegel, M. Dwyer, and P.D. Hovland, Correctness'17.
* [https://vsl.cis.udel.edu/lib/sw/civl/civl-manual.pdf  CIVL Manual], M.B. Dwyer, J. Edenhofner, G. Gopalakrishnan, A. Marianiello, Z. Luo, Z. Rakamaric, M. Rogers, S.F. Siegel, M. Zheng, and T.K. Zirkel
* [https://vsl.cis.udel.edu/pubs/civl_sc_2015.html CIVL: The Concurrency Intermediate Verification Language], S.F. Siegel, M. Zheng, Z. Luo, T.K. Zirkel, A.V. Marianiello, J.G. Edenhofner, M.B. Dwyer and M.S. Rogers, SC'15.
* [https://vsl.cis.udel.edu/pubs/civl_eurompi_2017.html  Verification of MPI programs using CIVL], Z. Luo, M. Zheng, and S.F. Siegel, EuroMPI'17.
* [https://science.energy.gov/~/media/ascr/pdf/programdocuments/docs/2017/HPC_Correctness_Report.pdf DOE Report of the HPC Correctness Summit], G. Gopalakrishnan, P.D. Hovland, C. Iancu, S. Krishnamoorthy, I. Laguna, R.A. Lethin, K. Sen, S.F. Siegel, and A. Solar-Lezama, DOE !TechReport'17.
* [https://vsl.cis.udel.edu/pubs/civl_verifythis_2016.html CIVL Solutions to VerifyThis 2016 Challenges], Stephen F. Siegel, !VerifyThis'16.
* [https://vsl.cis.udel.edu/pubs/civl_svcomp_2016.html CIVL: Applying a General Concurrency Verification Framework to C/Pthreads Programs Competition Contribution], M. Zheng, J.G. Edenhofner, Z. Luo, M.J. Gerrard, M.S. Rogers, M.B. Dwyer, and S.F. Siegel, TACAS'16
* [https://vsl.cis.udel.edu/pubs/civl_ase_2015.html CIVL: Formal Verification of Parallel Programs], M. Zheng, M.S. Rogers, Z. Luo, M.B. Dwyer, and S.F. Siegel, ASE'15.
* [https://vsl.cis.udel.edu/pubs/civl_tr_2014.html Tech Report: CIVL: The Concurrency Intermediate Verification Language], S.F. Siegel, M.B. Dwyer, G. Gopalakrishnan, Z. Luo, Z. Rakamaric, R. Thakur, M. Zheng, and T.K. Zirkel, Technical Report UD-CIS-2014/001.
* [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]

== License ==
CIVL is copyright from 2013 to 2018, Verified Software Laboratory, University of Delaware. 

CIVL is distributed under the terms of the [https://www.gnu.org/licenses/gpl.html GNU General Public License v3]. (See the directory licenses in the distribution for details.)