CIVL: Formal Verification of Parallel Programs

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.

@Inproceedings{zheng-etal:2015:civl_ase,
  author = {Manchun Zheng and Michael S.\ Rogers and Ziqing Luo 
            and Matthew B.\ Dwyer and Stephen F.\ Siegel},
  title = {{CIVL}: Formal Verification of Parallel Programs},
  booktitle = {ASE 2015: 30th IEEE/ACM International Conference on
               Automated Software Engineering, Proceedings},
  series = {ASE '15},
  year = {2015},
  month = {Nov},
  publisher = {IEEE Press},
  address = {Piscataway, NJ, USA},
  page = {830-835}
}