What ConcurInterproc does for you Contents

# What ConcurInterproc does for you

ConcurInterproc takes as input a "Simple" program, annotates it with control points, perform forward and/or backward analysis, and print the annotated programs with invariants associated with each control point, like this:

```
Annotated program after forward analysis:
var x : int, y : int, z : int
begin
/* (L5 C5) top */
assume z >= 10 and z <= 20; /* (L6 C25) [|-z+20>=0; z-10>=0|] */
x = 0; /* (L7 C8) [|x=0; -z+20>=0; z-10>=0|] */
y = 0; /* (L7 C13) [|-3x+y=0; -x+z+1>=0; -z+20>=0; z-10>=0; x>=0|] */
while x <= z do
/* (L8 C17) [|-3x+y=0; -x+z>=0; -z+20>=0; z-10>=0; x>=0|] */
x = x + 1; /* (L9 C12)
[|-3x+y+3=0; -x+z+1>=0; -z+20>=0; z-10>=0; x-1>=0|] */
y = y + 3; /* (L10 C12) [|-3x+y=0; -x+z+1>=0; -z+20>=0; z-10>=0; x-1>=0|] */
done; /* (L11 C7) [|-3x+y=0; -x+z+1=0; -x+21>=0; x-11>=0|] */
if y >= 42 then
/* (L12 C15) [|-3x+y=0; -x+z+1=0; -x+21>=0; x-14>=0|] */
fail; /* (L13 C9) bottom */
endif; /* (L14 C8) [|-3x+y=0; -x+z+1=0; -3x+41>=0; x-11>=0|] */
end
```

### Single forward/reachability analysis

A forward analysis computes (an overapproximation of) the set of reachable states of the program. It is displayed as formulas on variables describing their possible values at the associated control point.

### Single backward/coreachability analysis

A backward analysis computes (an overapproximation of) the set of states from which one can reach a fail instruction. This set is displayed under the same form as reachability.

### Combined forward/backward analyses

ConcurInterproc allows to combine forward and backward analysis any number of time.

If X denotes the invariant computed by ConcurInterproc at the previous step, at the current step:

• a forward analysis will consider the set of initial states

• a backward analysis will consider the set of final states

For instance, after executing the command

```  concurinterproc -analysis fb essai.spl
```

on the previous program, we get

```
Annotated program after forward analysis
var x : int, y : int, z : int
begin
/* (L5 C5) top */
assume z >= 10 and z <= 20; /* (L6 C25) [|-z+20>=0; z-10>=0|] */
x = 0; /* (L7 C8) [|x=0; -z+20>=0; z-10>=0|] */
y = 0; /* (L7 C13) [|-3x+y=0; -x+z+1>=0; -z+20>=0; z-10>=0; x>=0|] */
while x <= z do
/* (L8 C17) [|-3x+y=0; -x+z>=0; -z+20>=0; z-10>=0; x>=0|] */
x = x + 1; /* (L9 C12)
[|-3x+y+3=0; -x+z+1>=0; -z+20>=0; z-10>=0; x-1>=0|] */
y = y + 3; /* (L10 C12) [|-3x+y=0; -x+z+1>=0; -z+20>=0; z-10>=0; x-1>=0|] */
done; /* (L11 C7) [|-3x+y=0; -x+z+1=0; -x+21>=0; x-11>=0|] */
if y >= 42 then
/* (L12 C15) [|-3x+y=0; -x+z+1=0; -x+21>=0; x-14>=0|] */
fail; /* (L13 C9) bottom */
endif; /* (L14 C8) [|-3x+y=0; -x+z+1=0; -3x+41>=0; x-11>=0|] */
end

Annotated program after backward analysis
var x : int, y : int, z : int
begin
/* (L5 C5) [|-z+20>=0; z-13>=0|] */
assume z >= 10 and z <= 20; /* (L6 C25) [|-z+20>=0; z-13>=0|] */
x = 0; /* (L7 C8) [|x=0; -z+20>=0; z-13>=0|] */
y = 0; /* (L7 C13) [|-3x+y=0; -x+z+1>=0; -z+20>=0; z-13>=0; x>=0|] */
while x <= z do
/* (L8 C17) [|-3x+y=0; -x+z>=0; -z+20>=0; z-13>=0; x>=0|] */
x = x + 1; /* (L9 C12)
[|-3x+y+3=0; -x+z+1>=0; -z+20>=0; z-13>=0; x-1>=0|] */
y = y + 3; /* (L10 C12) [|-3x+y=0; -x+z+1>=0; -z+20>=0; z-13>=0; x-1>=0|] */
done; /* (L11 C7) [|-3x+y=0; -x+z+1=0; -x+21>=0; x-14>=0|] */
if y >= 42 then
/* (L12 C15) [|-3x+y=0; -x+z+1=0; -x+21>=0; x-14>=0|] */
fail; /* (L13 C9) bottom */
endif; /* (L14 C8) bottom */
end
```

 What ConcurInterproc does for you Contents