kirancodes.me
To Proof Maintenance & Beyond!
ASE 2015

CIVL: Formal Verification of Parallel Programs

Manchun Zheng, Michael S. Rogers, Ziqing Luo, Matthew B. Dwyer, Stephen F. Siegel

DOI 10.1109/ase.2015.99dblp

Abstract

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.

BibTeX
@inproceedings{Zheng-al:ASE15,
  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},
  pages     = {830--835},
  publisher = {{IEEE} Computer Society},
  year      = {2015},
}

Related papers