VSL Publications

CIVL: Applying a General Concurrency Verification Framework to C/Pthreads Programs (Competition Contribution)

Cite
Manchun Zheng, John G. Edenhofner, Ziqing Luo, Mitchell J. Gerrard, Michael S. Rogers, Matthew B. Dwyer, and Stephen F. Siegel. CIVL: Applying a General Concurrency Verification Framework to C/Pthreads Programs (Competition Contribution), Tools and Algorithms for the Construction and Analysis of Systems: 22nd International Conference, TACAS 2016, Eindhoven, The Netherlands, April 2–8, 2016, proceedings. Lecture Notes in Computer Science 9636, Springer-Verlag (2016), pages 908–911.
Abstract
CIVL is a framework for the analysis and verification of concurrent programs. The front-end translates C programs that use (subsets of) Pthreads, MPI, OpenMP, or CUDA––alone or in combination––to an intermediate verification language CIVL-C. The back-end uses symbolic execution and model checking techniques to verify a number of safety properties of a CIVL-C program, such as absence of assertion violations, deadlocks, or out-of-bound indexes. We submit CIVL for verifying Pthreads programs in the concurrency category.
Downloads
  1. civl_svcomp_2016.pdf (preprint)
Related Links
  1. CIVL executable for SVCOMP 2016
  2. Results of CIVL in SVCOMP 2016
BibTeX 
@Inproceedings{zheng-etal:2016:civl_tacas,
  author = {Manchun Zheng, John G.\ Edenhofner, Ziqing Luo, Mitchell J.\ Gerrard,
		Michael S.\ Rogers, Matthew B.\ Dwyer, and Stephen F.\ Siegel},
  title = {{CIVL}: Applying a General Concurrency Verification Framework to C/Pthreads
		Programs (Competition Contribution)},
  booktitle = {TACAS 16: International Conference on Tools and Algorithms
        for the Construction and Analysis of Systems, Proceedings},
  series = {TACAS '16},
  year = {2016},
  month = {Apr},
  publisher = {Springer-Verlag},
  address = {Eindhoven, The Netherlands},
}
VSL | Publications