[PPL-devel] [Fwd: Fwd: Info on PPL]

[Giorgio]

Enea,
  thanks a lot for the prompt reply.



> Giorgio Delzanno wrote:
>  > Enea,
>  > together with Ahmed Rezine (in cc) we'd like to use PPL for defining a
>  > sort of "extrapolation" method
>  > (to be applied as a subroutine of a verification process).
>  > To give you an example, suppose we compute (forward) a sequence of
>  > tuples of values
>  > (valuation of variables)  like (0,0) (1,1) (2,2)...
>  >  From this we would like to "extrapolate" the constraint X=Y without
>  > fixing in advance the
>  > shape of  equations (e.g. Y=MX+Q) we have to consider.
>  >
>  > Is there some kind of acceleration/widening that can be applied in this
>  > case?
>  > Thanks in advance,
>  > Giorgio
>  > ps: ... eventually, we started using PPL  :>
>  >
>  >
>
> Giorgio,
>
> the simple case above can be modeled using several (weakly) relational 
> abstract domains, such as polyhedra, octagonal shapes and BD shapes, and 
> probably using several variations of the standard widening of Cousot and 
> Halbwachs.
>
> Practically, suppose that you choose topologically closed polyhedra 
> (i.e., class C_Polyhedron in the C++ interface of the PPL), using the 
> standard widening (i.e., method H79_widening_assign in the C++ interface 
> of the PPL). Let P_0, P_1, ..., P_i, ... be the sequence of polyhedra, 
> where each P_i is a 2-dim polyhedron defined by the constraints
>    { x = i, y = i }.
> Then, you will end up computing the sequence of Q_i where
>
>    Q_0 := P_0 = { x = 0, y = 0 };
>
>    Q_1 := hull_1.H79_widening_assign(Q_0) = { x = y, y >= 0 },
>      where
>       hull_1 := the poly-hull of P_1 and Q_0
>               = { x = y, 0 <= y <= 1 }
>
>    Q_2 := hull_2.H79_widening_assign(Q_1) = Q_1 (fixpoint)
>      where
>       hull_2 := the poly-hull of P_2 and Q_1
>               = { x = y, 0 <= y <= 2 }
>
> Hope this is what you really meant.
>   
Ok. Is this the same as CH78  widening (based on constraint deletion)?
 We tried CC76_extrapolation on BDS but we probably forgot to compute 
the union.

To have a similar results for BDS, would it be correct to use something like

bds1= x=0,y=0
bds2= x=1,y=1

bds2=upper_bound_assign(bds1);   // smallest bds union of bds1 and bds2
bd2=bds2.H79_widening_assign(bds1);

(I am writing from home and cannot test it right now).
Thanks,
 Giorgio & Ahmed