| 3 | | == Abstract == |
| 4 | | '''CIVL: Concurrency Intermediate Verification Language''' is a framework for the verification of multiple concurrent C dialects and libraries, such as OpenMP, MPI, Pthreads, CUDA, etc. |
| 5 | | It contains transformers to transform programs of such language or libraries into CIVL-C program, which is a dialect of C with concurrent extension, and uses symbolic execution to model check the programs. |
| 6 | | CIVL-C language is designed to capture the common features of concurrency so that could be used to describe a large number of concurrent dialects or libraries. |
| 7 | | CIVL is open source, and is designed to be flexible to be extended for verifying more concurrent languages and libraries. |
| 8 | | |
| 9 | | Properties that CIVL checks include: deadlock, memory leak, array index-out-of bound, invalid pointer dereference, user-specified assertions, and functional equivalence. |
| 10 | | |
| 11 | | CIVL is also able to verify hybrid concurrent programs, i.e., programs containing more than one dialects or librabries, such as MPI-OpenMP, MPI-Pthreads, etc. |
| 12 | | |
| 13 | | == Examples == |
