VSL Publications

CIVL: Formal Verification of Parallel Programs

Manchun Zheng, Michael S. Rogers, Ziqing Luo, Matthew B. Dwyer, and Stephen F. Siegel, CIVL: Formal Verification of Parallel Programs. ASE 2015: 30th IEEE/ACM International Conference on Automated Software Engineering, Lincoln, Nebraska, USA, Nov 9–13, 2015, pages 830-835.
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.
  1. civl_ase_2015.pdf (preprint)
  2. civl_experiments_ase_2015.tgz (experimental archive with source code)
Related Links
  1. CIVL demo page
  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}

VSL | Publications