| 1 |
|
|---|
| 2 | <html>
|
|---|
| 3 | <body>
|
|---|
| 4 |
|
|---|
| 5 | <p>Welcome to CIVL, the Concurrency Intermediate Verification Language tool.
|
|---|
| 6 | CIVL is a Java project for verifying concurrent programs written in CIVL-C,
|
|---|
| 7 | which is a C dialect with extensions to concurrent language constructs.
|
|---|
| 8 | The CIVL project uses ABC, SARL and GMC.
|
|---|
| 9 | The CIVL tool can be used to perform a number of tasks, including the following:
|
|---|
| 10 | <ol>
|
|---|
| 11 | <li>preprocess or pass a CIVL-C program;</i>
|
|---|
| 12 | <li>verify a CIVL-C program;</li>
|
|---|
| 13 | <li>run a CIVL-C program;</li>
|
|---|
| 14 | <li>replay traces for a program.</li>
|
|---|
| 15 | </ol>
|
|---|
| 16 |
|
|---|
| 17 | In addition, it provides a framework for developing your own libraries
|
|---|
| 18 | or transformations on ASTs of various language extensions and libraries.
|
|---|
| 19 | </p>
|
|---|
| 20 |
|
|---|
| 21 | There is a simple command-line interface for CIVL (see {@link
|
|---|
| 22 | edu.udel.cis.vsl.civl.CIVL CIVL}), but most users will want to use CIVL
|
|---|
| 23 | through its API. To use the API, it is helpful to have some
|
|---|
| 24 | understanding of the modular structure of CIVL. The CIVL source code is
|
|---|
| 25 | decomposed into modules, each with a well-defined interface and set of
|
|---|
| 26 | responsibilities. Some of these modules are decomposed further into
|
|---|
| 27 | sub-modules. The top-level modules are:
|
|---|
| 28 | <ol>
|
|---|
| 29 |
|
|---|
| 30 | <li><strong>util</strong>
|
|---|
| 31 | <ol>
|
|---|
| 32 | <li>responsibilities: simple general-purpose utility classes
|
|---|
| 33 | that do not use other parts of CIVL</li>
|
|---|
| 34 | <li>uses: nothing</li>
|
|---|
| 35 | <li>interface: {@link edu.udel.cis.vsl.civl.util.IF}</li>
|
|---|
| 36 | <li>entry point: none</li>
|
|---|
| 37 | </ol></li>
|
|---|
| 38 |
|
|---|
| 39 | </ol>
|
|---|
| 40 |
|
|---|
| 41 | </body>
|
|---|
| 42 | </html>
|
|---|
| 43 |
|
|---|
