Automated Verification of Scientific Software

CIVL is a verifier for scientific and concurrent programs. The tool accepts C programs, including concurrent C programs that use certain subsets of MPI, OpenMP, Pthreads, or CUDA. There is also support for Fortran. Using symbolic execution and model checking techniques, CIVL can verify the absence of assertion violations, deadlocks, data races, memory leaks, illegal pointer operations, and other runtime errors. It can also be used to verify the functional equivalence of two programs. CIVL has been used to check correctness of performance optimizations, refactoring, and parallelization, and to distinguish roundoff errors from other program defects. CIVL translates all programs into a general intermediate verification language, CIVL-C, but users can also write CIVL-C programs directly. While CIVL typically requires small bounds on the number of processes/threads and on other program parameters, it verifies programs for all possible inputs and behaviors within the specified scope, and is effective at finding and explaining defects.

  Coming.