Changes between Version 2 and Version 3 of Introduction


Ignore:
Timestamp:
12/21/18 13:42:16 (7 years ago)
Author:
siegel
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • Introduction

    v2 v3  
    55* [#lang Language]
    66* [#semantics Semantics]
    7 * [# tools Tools]
     7* [#tools Tools]
    88
    99= Introduction = #intro
     10
     11== What is CIVL? ==
     12
     13CIVL stands for ''Concurrency Intermediate Verification Language''.  The CIVL platform encompasses:
     14
     151. the programming language CIVL-C, a dialect of C with additional primitives supporting concurrency, specification, and modeling;
     161. verification and analysis tools, including a symbolic execution-based model checker for checking various properties of, or finding defects in, CIVL-C programs; and
     171. tools that translate from many commonly used languages/APIs to CIVL-C.
     18
     19The 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.
     20
     21This manual covers all aspects of the CIVL framework, and is organized in parts as follows:
     22
     231. this introduction, including "quick start" instructions for downloading and installing CIVL and several examples;
     241. a complete description of the CIVL-C language;
     251. a formal semantics for the language; and
     261. a description of the tools in the framework.
     27
     28== Installation and Quick Start ==
     29
     30== Examples ==
     31
     32== Verifying  Programs ==
     33
     34=== Verifying C Programs ===
     35
     36=== Verifying C/MPI Programs ===
     37
     38=== Verifying C/OpenMP Programs ===
     39
     40=== Verifying CUDA-C Programs ===
     41
     42=== Verifying C/Pthreads Programs ===
     43
     44=== Verifying Fortran Programs ===
     45
     46(under development)
     47
    1048
    1149