Skip to content

The CIVL Model Checker

About

The CIVL model checker is a verification tool for sequential or parallel programs. It targets primarily C programs, including parallel C programs that use OpenMP or MPI, and CUDA-C programs. The general verification approach is based on model checking and symbolic execution.

The verifier uses a concurrency intermediate verification language, CIVL-C. Users may write in CIVL-C directly; this is a good way to prototype algorithms. One may also start from standard C (or CUDA-C), which the tool first translates to CIVL-C. CIVL may also be applied to programs composed of multiple translation units, some of which are in CIVL-C and others in C or CUDA-C.

CIVL can verify a number of safety properties, including absence of assertion violations, deadlocks, memory leaks, illegal pointer dereferences, out-of-bound array indexes, and divisions by zero. In most cases, this requires placing relatively small bounds on the size of inputs and/or the numbers of threads or processes. In any case, when a violation is found, detailed diagnostic information is provided, including a (minimal) execution trace terminating in a violating state.

CIVL currently supports only subsets of the languages and language extensions mentioned above. We are continually expanding these subsets, prioritizing the most commonly-used language features.

Documentation

Publications

How to Cite CIVL

@Inproceedings{siegel-etal:2015:civl_sc,
  author = {Stephen F.\ Siegel and Manchun Zheng and Ziqing Luo and
            Timothy K.\ Zirkel and Andre V.\ Marianiello and John G.\ Edenhofner
            and Matthew B.\ Dwyer and Michael S.\ Rogers},
  title = {{CIVL}: The Concurrency Intermediate Verification Language},
  booktitle = {SC15: International Conference for High Performance
               Computing, Networking, Storage and Analysis, Proceedings},
  series = {SC '15},
  year = {2015},
  month = {Nov},
  publisher = {IEEE Press},
  address = {Piscataway, NJ, USA},
  pages = {61:1-61:12},
  doi = {10.1145/2807591.2807635}
}

Bug Reports

To report a bug in CIVL, either create a GitHub issue or send an email to civl-dev@googlegroups.com. Include as many details as possible, such as the CIVL command, source files (these may be attached), the CIVL version, and the output, including any error message.

Developers

  • Current Developers: Stephen Siegel and Alex Wilton
  • Previous Contributors: Matthew Dwyer, John Edenhofner, Mitchell Gerrard, Ziqing Luo, Andre Marianiello, Michael Rogers, Wenhao Wu, Yihao Yan, Manchun Zheng and Timothy Zirkel

DeveloperPage

License

CIVL is copyright from 2013 to 2026, Verified Software Laboratory, Department of Computer and Information Sciences, University of Delaware.

CIVL is distributed under the terms of the GNU General Public License v3. (See the directory licenses in the distribution for details.)