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
