CIVL: The Concurrency Intermediate Verification Language

Recent years have witnessed an explosion in the number of programming languages and language extensions dealing with concurrency. Examples include message-passing libraries (MPI-3), multithreading and GPU language extensions such as OpenMP, Pthreads, OpenCL, and CUDA, and entirely new languages such as Chapel. 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 between efforts. To address this problem, we present CIVL: a Concurrency Intermediate Verification Language. CIVL provides a concurrency model suciently flexible to represent programs in a wide variety of parallel languages, including those listed above. We have realized CIVL as a dialect of C with new primitives for concurrency and others to facilitate specification and verification. We have also developed a tool that combines model checking and symbolic execution to verify or refute a number of properties of CIVL programs, such as freedom from deadlock and assertion violations.

@TechReport{siegelDGLRTZZ:2014:civl-tr,
	author = {Stephen F. Siegel and Matthew B. Dwyer and Ganesh Gopalakrishnan 
	          and Ziqing Luo and Zvonimir Rakamaric and Rajeev Thakur 
	          and Manchun Zheng and Timothy K. Zirkel},
	title = {CIVL: The Concurrency Intermediate Verification Language},
	institution = {Department of Computer and Information Sciences,
	University of Delaware},
	year = {2014},
	number = {UD-CIS-2014/001}
}