Changes between Version 20 and Version 21 of Introduction

Timestamp:

12/31/18 14:59:06 (7 years ago)

Author:

siegel

Comment:

--

Introduction

@@ -1 @@
-
-= Contents =
 
 [[PageOutline]]
 
-= What is CIVL? =
+= CIVL Manual: Introduction =
+
+== What is CIVL? ==
 
 CIVL stands for ''Concurrency Intermediate Verification Language''.  The CIVL platform encompasses:
@@ -43 +43 @@
 
 
-= Verifying CIVL-C Programs =
+== Verifying CIVL-C Programs ==
 
 Dijkstra’s well-known Dining Philosophers system can be encoded in CIVL-C as follows:
@@ -418 +418 @@
 
 
-= Verifying Sequential C Programs =
+== Verifying Sequential C Programs ==
 
 Since almost anything you can do in sequential C is also legal CIVL-C, there is not much you have to do to apply the verifier to C programs.
@@ -575 +575 @@
 There are limitations to the application of CIVL to C programs.   Support for the standard library is only partial.   Small bounds will have to be placed on many parameters in order for CIVL verification to terminate (or terminate in a reasonable amount of time).  
 
-= Verifying C/MPI Programs =
+== Verifying C/MPI Programs ==
 
 CIVL can verify C/MPI programs that use a subset of MPI.    The instructions for sequential programs apply equally to MPI programs.  In addition, one must specify either (1) the number of processes for the MPI program, or (2) an upper and a lower bound on the number of processes for the MPI program.
@@ -593 +593 @@
 
 
-= Verifying C/OpenMP Programs =
+== Verifying C/OpenMP Programs ==
 
 CIVL uses an input variable `omp_thread_max` for verifying OpenMP programs.   It must be specified on the command line, e.g.,
@@ -607 +607 @@
 A serious limitation in the current OpenMP transformation is that access to shared variables cannot take place through pointers.
 
-= Verifying CUDA-C Programs =
-
-
-
-= Verifying C/Pthreads Programs =
-
-
-
-= Verifying Fortran Programs =
-
+== Verifying CUDA-C Programs ==
+
+
+
+== Verifying C/Pthreads Programs ==
+
+
+
+== Verifying Fortran Programs ==