January 2009 - PPL-devel - BUGSENG Mailman

w3ppl/htdocs/Documentation ppl_citations.bib
by Roberto Bagnara 20 Jan '09

20 Jan '09

CVSROOT: /cvs/ppl Module name: w3ppl Changes by: bagnara(a)cs.unipr.it 2009-01-20 21:26:49 Modified files: htdocs/Documentation: ppl_citations.bib Log message: Added LavironL09. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/w3ppl/htdocs/Documentation/ppl_ci…

1 0

Fwd: Info on PPL
by Enea Zaffanella 20 Jan '09

20 Jan '09

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(a)cs.unipr.it.

1 0

w3ppl/htdocs/Documentation ppl_citations.bib
by Roberto Bagnara 20 Jan '09

20 Jan '09

CVSROOT: /cvs/ppl Module name: w3ppl Changes by: bagnara(a)cs.unipr.it 2009-01-20 21:16:09 Modified files: htdocs/Documentation: ppl_citations.bib Log message: Added GulwaniL-AS09. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/w3ppl/htdocs/Documentation/ppl_ci…

1 0

ppl/demos/ppl_lpsol ppl_lpsol.c
by Roberto Bagnara 20 Jan '09

20 Jan '09

CVSROOT: /cvs/ppl Module name: ppl Changes by: bagnara(a)cs.unipr.it 2009-01-20 18:56:57 Modified files: demos/ppl_lpsol: ppl_lpsol.c Log message: Fixed glpk_message_interceptor() (thanks to Kenneth MacKenzie). Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/demos/ppl_lpsol/ppl_lpsol.c.d…

1 0

ppl/tests/Octagonal_Shape upperboundifexact1.cc
by Enea Zaffanella 20 Jan '09

20 Jan '09

CVSROOT: /cvs/ppl Module name: ppl Changes by: zaffanella(a)cs.unipr.it 2009-01-20 18:27:04 Modified files: tests/Octagonal_Shape: upperboundifexact1.cc Log message: Added test on (higher dimensional) hypercubes. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/tests/Octagonal_Shape/upperbo…

1 0

ppl/src Octagonal_Shape.templates.hh
by Enea Zaffanella 20 Jan '09

20 Jan '09

CVSROOT: /cvs/ppl Module name: ppl Changes by: zaffanella(a)cs.unipr.it 2009-01-20 18:21:55 Modified files: src : Octagonal_Shape.templates.hh Log message: The code fo rthe detection of non-redundant octagonal constraints factored out of the strong reduction assign method into the new private method non_redundant_matrix_entries(), so that it can be reused in other contexts. In particular, now we also use it in the implementation of upper_bound_assign_if_exact(). Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Octagonal_Shape.templates…

1 0

ppl/src Octagonal_Shape.defs.hh
by Enea Zaffanella 20 Jan '09

20 Jan '09

CVSROOT: /cvs/ppl Module name: ppl Changes by: zaffanella(a)cs.unipr.it 2009-01-20 18:14:21 Modified files: src : Octagonal_Shape.defs.hh Log message: Declared a new (private) method that is meant to identify the non-redundant octagonal constraints without actually computing a strongly reduced matrix. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/Octagonal_Shape.defs.hh.d…

1 0

ppl/tests/BD_Shape upperboundifexact1.cc
by Enea Zaffanella 20 Jan '09

20 Jan '09

CVSROOT: /cvs/ppl Module name: ppl Changes by: zaffanella(a)cs.unipr.it 2009-01-20 10:00:38 Modified files: tests/BD_Shape : upperboundifexact1.cc Log message: Added a test on hypercubes. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/tests/BD_Shape/upperboundifex…

1 0

ppl/src BD_Shape.templates.hh
by Enea Zaffanella 20 Jan '09

20 Jan '09

CVSROOT: /cvs/ppl Module name: ppl Changes by: zaffanella(a)cs.unipr.it 2009-01-20 09:59:24 Modified files: src : BD_Shape.templates.hh Log message: Method BHZ09_upper_bound_assign_if_exact() improved by exploiting shortest path reduction so as to avoid checks on redundant constraints. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/ppl/src/BD_Shape.templates.hh.dif…

1 0

w3ppl/htdocs/Links Links.raw
by Roberto Bagnara 19 Jan '09

19 Jan '09

CVSROOT: /cvs/ppl Module name: w3ppl Changes by: bagnara(a)cs.unipr.it 2009-01-19 17:37:47 Modified files: htdocs/Links : Links.raw Log message: Added links to "Using git without feeling stupid", by Paolo Bonzini. Patches: http://www.cs.unipr.it/cgi-bin/cvsweb.cgi/w3ppl/htdocs/Links/Links.raw.diff…

1 0