_            _    _        _         _
      /\ \         /\ \ /\ \     /\_\      / /\
      \_\ \       /  \ \\ \ \   / / /     / /  \
      /\__ \     / /\ \ \\ \ \_/ / /     / / /\ \__
     / /_ \ \   / / /\ \ \\ \___/ /     / / /\ \___\
    / / /\ \ \ / / /  \ \_\\ \ \_/      \ \ \ \/___/
   / / /  \/_// / /   / / / \ \ \        \ \ \
  / / /      / / /   / / /   \ \ \   _    \ \ \
 / / /      / / /___/ / /     \ \ \ /_/\__/ / /
/_/ /      / / /____\/ /       \ \_\\ \/___/ /
\_\/       \/_________/         \/_/ \_____\/
civl 1.22
Dependencies: antlr3@3.5.2 antlr4@4.10.1 why3@1.7.2 z3@4.13.0 java-antlr4-runtime@4.10.1 java-stringtemplate@4.0.8
Channel: loftix
Location: loftix/model-checking.scm (loftix model-checking)
Home page: https://vsl.cis.udel.edu/trac/civl/wiki
Licenses: GPL 3
Build system: ant
Synopsis: Concurrency intermediate verification language
Description:

CIVL is a framework encompassing

  • a programming language, CIVL-C, which adds to C a number of concurrency primitives, as well as the to define functions in any scope. Together, these features make for a very expressive concurrent language that can faithfully represent programs using various APIs and parallel languages, such as MPI, OpenMP, CUDA, and Chapel. CIVL-C also provides a number of primitives supporting verification.

  • a model checker which uses symbolic execution to verify a number of safety properties of CIVL-C programs. The model checker can also be used to verify that two CIVL-C programs are functionally equivalent.

  • a number of translators from various commonly-used concurrency languages/APIs to CIVL-C (currently, MPI, OpenMP, Pthreads, and CUDA).

Total results: 1