
11 Feb
2016
11 Feb
'16
7:05 a.m.
Hello Bishoksan.
On 02/10/2016 09:47 PM, Bishoksan Kafle wrote:
- 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.
- 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@cs.unipr.it
BUGSENG srl - http://bugseng.com
mailto:roberto.bagnara@bugseng.com