# The CIVL Model Checker

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. 

For more information about CIVL, including installation instructions,
language documentation, and examples, see
[the CIVL documentation](https://verified-software-lab.github.io/civl/).