[PPL-devel] Fwd: Info on PPL
Enea Zaffanella
zaffanella at cs.unipr.it
Tue Jan 20 21:23:52 CET 2009
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.
Cheers,
Enea.
P.S.: Please, direct all PPL-related messages to ppl-devel at cs.unipr.it.
More information about the PPL-devel
mailing list