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

• Latest stable release: ​http://vsl.cis.udel.edu/lib/sw/civl/current/latest/
• Latest unstable release: ​http://vsl.cis.udel.edu/lib/sw/civl/trunk/latest/
• Older releases: ​http://vsl.cis.udel.edu/lib/sw/civl/
• Online application: ​http://civl.cis.udel.edu/app/

Examples & Case Studies

• A Brief Tour of CIVL with Examples
• ​CIVL Solutions to VerifyThis 2016 Challenges
• ​Towards Self-Verification in Finite Difference Code Generation
• ​Verifying Properties of Differentiable Programs

Documents & Publications

• ​Manual for CIVL v1.16
• ​CIVL Solutions to VerifyThis 2016 Challenges
• ​Verification of MPI programs using CIVL

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 Report

If you have any problem when using CIVL, you can report it by creating a new ticket: https://vsl.cis.udel.edu/trac/civl/newticket.
It would be helpful for us to trace the bug if you also submit your source programs as attachments of the ticket.

When reporting a bug, you are greatly recommended to provide specific information as much as possible, such as the civl command, the source files, the civl version, the error message or exception, etc. The minimum is to provide sufficient information for others to reproduce the problem.