[PPL-devel] Narrowing for polyhedral domains

[Roberto Bagnara]

On 11/07/12 16:34, Zhoulai wrote:
> This may be a silly question. But I would like to know why narrowing
> for polyhedral domains is not implemented in PPL?  I recently
> experienced many cases where analysis using Int64_Box gives more
> precise results than NNC_Polyhedral because the former provides a
> narrowing.
>
> What do you think?

Dear Zell,

the study of narrowing operators for the domain of (C or NNC) polyhedra
has not received much attention.  This is due in part to the fact that
there is little incentive.  Intersection (the domain glb) satisfies
the first part of the definition of narrowing operator (that it yields
a lower bound of the argument) in the most precise way;  the second
part of the definition (eventual stabilization of the decreasing iteration
sequence) can be dispensed with: just enforce an external limit to the
length of the decresing iteration sequence and you are done.
Experience shows that decreasing iterations sequences longer than 1
often give little or no extra precision.
Kind regards,

     Roberto

-- 
      Prof. Roberto Bagnara

Applied Formal Methods Laboratory - University of Parma, Italy
mailto:bagnara at cs.unipr.it
                               BUGSENG srl - http://bugseng.com
                               mailto:roberto.bagnara at bugseng.com