Changes between Version 3 and Version 4 of Introduction

Timestamp:

12/21/18 13:56:09 (7 years ago)

Author:

siegel

Comment:

--

Introduction

@@ -15 +15 @@
 1. the programming language CIVL-C, a dialect of C with additional primitives supporting concurrency, specification, and modeling;
 1. verification and analysis tools, including a symbolic execution-based model checker for checking various properties of, or finding defects in, CIVL-C programs; and
-1. tools that translate from many commonly used languages/APIs to CIVL-C.
+1. tools that translate from 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.
+A user can write programs in CIVL-C directly, or use one of the front-ends that translates from a "real" programming language to CIVL-C.
+
+When used in the first way, CIVL-C may be considered a modeling language, similar to Promela (the language used by the model checker Spin).  This is useful for exploring and verifying algorithms, especially concurrent algorithms.  The main difference between CIVL-C and Promela is that CIVL-C includes almost all of the language constructs in C, including floating-point numbers, arrays of any type, structs, functions, pointers,  dynamic allocation (malloc and free), and pointer arithmetic.    Like Spin, the CIVL verifier can be used to perform an exhaustive search of a state space.  Unlike Spin, the CIVL verifier uses symbolic execution, so in a CIVL state, variables may be assigned symbolic expressions, not just concrete values.   This allows the verifier to check properties of the form ''the assertions hold for all possible inputs'' and ''the two given programs are functionally equivalent.''
+
+When used in the second way, a C program using MPI, CUDA, OpenMP, or Pthreads, (or even some combination of these 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: