some questions regarding PPL
Hi PPL-developers
I would be glad if you could help me find answers to the following questions:
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?
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, but in the user manual I found the following text:
[cid:BC9F6334-FB66-4E2B-BE47-2E4A8D844CD6]
What are the differences between these two functions? Do they differ in precision? complexity?
3. What is the function corresponding to poly_hull_assign for Octagon?
Many thanks in advance Bishoksan
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
On Feb 11, 2016, at 8:05 AM, Roberto Bagnara <bagnara@cs.unipr.itmailto:bagnara@cs.unipr.it> wrote:
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?
Sorry I wanted to ask the difference between poly-hull and convex-hull. Please ignore my previous question.
thank you Bishoksan
On 02/11/2016 09:17 PM, Bishoksan Kafle wrote:
On Feb 11, 2016, at 8:05 AM, Roberto Bagnara <bagnara@cs.unipr.it mailto:bagnara@cs.unipr.it> wrote:
- 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?
Sorry I wanted to ask the difference between poly-hull and convex-hull. Please ignore my previous question.
The convex polyhedral hull of a set of convex polyhedra P is the smallest convex polyhedron that contains all members of P.
The convex hull of a set of convex polyhedra P is the smallest convex set that contains all members of P.
There exists P such that convex_polyhedral_hull(P) != convex_hull(P). For instance, take P = { p1, p2 } where:
p1 = { (x, y) in R^2 | x = 0 }, p2 = { (x, y) in R^2 | x = 0, y = 1 }.
We have that (1, 1) belongs to convex_polyhedral_hull(P) but (1, 1) does *not* belong to convex_hull(P). Kind regards,
Roberto
On Feb 12, 2016, at 8:03 AM, Roberto Bagnara bagnara@cs.unipr.it wrote:
On 02/11/2016 09:17 PM, Bishoksan Kafle wrote:
On Feb 11, 2016, at 8:05 AM, Roberto Bagnara <bagnara@cs.unipr.it mailto:bagnara@cs.unipr.it> wrote:
- 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?
Sorry I wanted to ask the difference between poly-hull and convex-hull. Please ignore my previous question.
The convex polyhedral hull of a set of convex polyhedra P is the smallest convex polyhedron that contains all members of P.
The convex hull of a set of convex polyhedra P is the smallest convex set that contains all members of P.
There exists P such that convex_polyhedral_hull(P) != convex_hull(P). For instance, take P = { p1, p2 } where:
p1 = { (x, y) in R^2 | x = 0 }, p2 = { (x, y) in R^2 | x = 0, y = 1 }.
We have that (1, 1) belongs to convex_polyhedral_hull(P) but (1, 1) does *not* belong to convex_hull(P).
I see your point, but do you mean p2 = { (x, y) in R^2 | x = 1, y = 1 } instead of p2 = { (x, y) in R^2 | x = 0, y = 1 }?
thank you Bishoksan
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
On 02/12/2016 02:00 PM, Bishoksan Kafle wrote:
On Feb 12, 2016, at 8:03 AM, Roberto Bagnara bagnara@cs.unipr.it wrote:
On 02/11/2016 09:17 PM, Bishoksan Kafle wrote:
On Feb 11, 2016, at 8:05 AM, Roberto Bagnara <bagnara@cs.unipr.it mailto:bagnara@cs.unipr.it> wrote:
- 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?
Sorry I wanted to ask the difference between poly-hull and convex-hull. Please ignore my previous question.
The convex polyhedral hull of a set of convex polyhedra P is the smallest convex polyhedron that contains all members of P.
The convex hull of a set of convex polyhedra P is the smallest convex set that contains all members of P.
There exists P such that convex_polyhedral_hull(P) != convex_hull(P). For instance, take P = { p1, p2 } where:
p1 = { (x, y) in R^2 | x = 0 }, p2 = { (x, y) in R^2 | x = 0, y = 1 }.
We have that (1, 1) belongs to convex_polyhedral_hull(P) but (1, 1) does *not* belong to convex_hull(P).
I see your point, but do you mean p2 = { (x, y) in R^2 | x = 1, y = 1 } instead of p2 = { (x, y) in R^2 | x = 0, y = 1 }?
Sorry, I mistyped it by swapping x and y in p2: I meant
p1 = { (x, y) in R^2 | x = 0 }, p2 = { (x, y) in R^2 | x = 1, y = 0 }.
We have that (1, 1) belongs to convex_polyhedral_hull(P) but (1, 1) does *not* belong to convex_hull(P).
Kind regards,
Roberto
participants (2)
-
Bishoksan Kafle -
Roberto Bagnara