[PPL-devel] some questions regarding PPL

[Roberto Bagnara]

Hello Bishoksan.

On 02/10/2016 09:47 PM, Bishoksan Kafle wrote:
> 1. Having software verification in mind (problems over integers)
> which abstract domain(s) (more precisely domains provided by PPL)
> provide good trade-off between complexity and expressiveness?

There is no definite answer to this question: it all depends on
what you consider a "good trade-off" and on the nature and dimension
of the verification problems you want to solve.  You employ techniques
to reduce the number of variables, use timeouts, ... there are many
possibilities.  Luckily, with the PPL it is relatively easy to
make experiments.

> 2. In the article
> (http://bugseng.com/products/ppl/documentation/BagnaraRZH02.pdf),
> you mentioned that poly_hull_assign is different from
> upper_bound_assign for Polyhedra

Where exactly do you read that?
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