Contents

• Introduction
• Language
• Semantics
• Tools

Introduction

What is CIVL?

CIVL stands for Concurrency Intermediate Verification Language. The CIVL platform encompasses:

1. the programming language CIVL-C, a dialect of C with additional primitives supporting concurrency, specification, and modeling;
2. verification and analysis tools, including a symbolic execution-based model checker for checking various properties of, or finding defects in, CIVL-C programs; and
3. tools that translate from many commonly used languages/APIs to CIVL-C.

The CIVL-C language is primarily intended to be an intermediate representation for verification. A C program using MPI, CUDA, OpenMP, Pthreads, or another API (or even some combination of APIs), will be automatically translated into CIVL-C and then verified. The advantages of such a framework are clear: the developer of a new verification technique could implement it for CIVL-C and then immediately see its impact across a broad range of concurrent programs. Likewise, when a new concurrency API is introduced, one only needs to implement a translator from it to CIVL-C in order to reap the benefits of all the verification tools in the platform. Programmers would have a valuable verification and debugging tool, while API designers could use CIVL as a "sandbox" to investigate possible API modifications, additions, and interactions.

This manual covers all aspects of the CIVL framework, and is organized in parts as follows:

1. this introduction, including "quick start" instructions for downloading and installing CIVL and several examples;
2. a complete description of the CIVL-C language;
3. a formal semantics for the language; and
4. a description of the tools in the framework.

Installation and Quick Start

Examples

Verifying Programs

Verifying C Programs

Verifying C/MPI Programs

Verifying C/OpenMP Programs

Verifying CUDA-C Programs

Verifying C/Pthreads Programs

Verifying Fortran Programs

(under development)

Language

Semantics

Tools