| 1 |
|
|---|
| 2 | Part I: Introduction
|
|---|
| 3 |
|
|---|
| 4 | Chpater: What CIVL is all about: purpose, verification, CIVL-C, tools,
|
|---|
| 5 | organization of this document
|
|---|
| 6 | Chapter: Installation and Quick Start
|
|---|
| 7 | Chpater: Some examples
|
|---|
| 8 |
|
|---|
| 9 | Part II: Language
|
|---|
| 10 |
|
|---|
| 11 | Chapter: Language overview
|
|---|
| 12 | Key concepts: static scope tree, nested functions, dynamic scope tree
|
|---|
| 13 | Examples!
|
|---|
| 14 | C, Syntax, #include<civlc.h> $ sign, nested functions,
|
|---|
| 15 | processes, spawning, waiting, types, ...
|
|---|
| 16 |
|
|---|
| 17 | Chapter: Structure of program
|
|---|
| 18 | preprocessor directives
|
|---|
| 19 | function prototypes and definitions
|
|---|
| 20 | lexical scopes and the lexical scope tree
|
|---|
| 21 | naming scopes ($scope)
|
|---|
| 22 | translation of source to model
|
|---|
| 23 | root function, root scope and the main function
|
|---|
| 24 | formal parameters to main, return value
|
|---|
| 25 |
|
|---|
| 26 | Chapter: Sequential elements
|
|---|
| 27 | Section: types:
|
|---|
| 28 | inherited from C: integer and real, boolean, arrays pointer
|
|---|
| 29 | bundles
|
|---|
| 30 | sequences int a[<i>] (coming)
|
|---|
| 31 | Section: expressions (currently missing: bitwise,...)
|
|---|
| 32 | Section: statements inherited from C : for, while, {...}
|
|---|
| 33 | goto, labeled statements, switch, case, default,
|
|---|
| 34 | break, continue, ...
|
|---|
| 35 | Section: Nondeterminism:
|
|---|
| 36 | $choose/$when
|
|---|
| 37 | $choose_int
|
|---|
| 38 |
|
|---|
| 39 | Chapter: Concurrency
|
|---|
| 40 | section: Process creation and magagement: $proc type, $spawn, $wait, $self
|
|---|
| 41 | return value of spawned function (must be function returning void?)
|
|---|
| 42 | section: dynamic scope tree, revisited, and the state of a CIVL program
|
|---|
| 43 | section: Atomicity: $atom, $atomic, guards and $when
|
|---|
| 44 | section: Message Passing
|
|---|
| 45 |
|
|---|
| 46 | Chapter: Specification
|
|---|
| 47 | section: overview, and pointer to concurrency section for more
|
|---|
| 48 | specification primitivies
|
|---|
| 49 | section: input/output signature: $input, $output
|
|---|
| 50 | section: assertions and assumptions: $assert, $assume, $invariant
|
|---|
| 51 | section: assertion language: $forall, $exists, => (implies)
|
|---|
| 52 | (in addition to &&, ||, !)
|
|---|
| 53 | section: procedure contracts, $ensures, $requires (coming)
|
|---|
| 54 | section: Concurrency specification: remote expressions, collective expressions
|
|---|
| 55 |
|
|---|
| 56 | Chapter: Pointers and Heaps
|
|---|
| 57 | $malloc, $free, memcpy
|
|---|
| 58 | scope-parameterized pointers
|
|---|
| 59 |
|
|---|
| 60 | Chapter: Libraries
|
|---|
| 61 | The following can be included to provide additional primitives:
|
|---|
| 62 | (in addition to civlc.h):
|
|---|
| 63 | stdbool.h
|
|---|
| 64 | stdio.h
|
|---|
| 65 | stdlib.h
|
|---|
| 66 | assert.h
|
|---|
| 67 |
|
|---|
| 68 |
|
|---|
| 69 | Part III: Semantics
|
|---|
| 70 | The formal description of semantics
|
|---|
| 71 |
|
|---|
| 72 |
|
|---|
| 73 | Part IV: Tools
|
|---|
| 74 | Chapter: Tool introduction
|
|---|
| 75 | section: symbolic execution (background)
|
|---|
| 76 | section: tool overview, command line civl, civl help
|
|---|
| 77 | Chapter: running a CIVL-C program
|
|---|
| 78 | Chapter: model checking, options
|
|---|
| 79 | Chapter: replaying counter-examples
|
|---|
| 80 | Chapter: MPI programs
|
|---|
| 81 |
|
|---|
