CIVL is a framework for static analysis and verification of concurrent programs. One of the main challenges to practical application of these techniques is the large number of ways to express concurrency: MPI, OpenMP, CUDA, and Pthreads, for example, are just a few of many "concurrency dialects" in wide use today. These dialects are constantly evolving and it is increasingly common to use several of them in a single "hybrid" program. CIVL addresses these problems by providing a concurrency intermediate verification language, CIVL-C, as well as translators that consume C programs using these dialects and produce CIVL-C. Analysis and verification tools which operate on CIVL-C can then be applied easily to a wide variety of concurrent C programs. We demonstrate CIVL's error detection and verification capabilities on (1) an MPI+OpenMP program that estimates π and contains a subtle race condition, and (2) an MPI-based 1d-wave simulator that fails to conform to a simple sequential implementation.

There are many ways to express parallel programs: message-passing libraries (MPI) and multithreading/GPU language extensions such as OpenMP, Pthreads, and CUDA, are but a few. This multitude creates a serious challenge for developers of software verification tools: it takes enormous effort to develop such tools, but each development effort typically targets one small part of the concurrency landscape, with little sharing of techniques and code among efforts.