What ConcurInterproc does for youContents

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:

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 youContents