
<html>

<head>

<meta http-equiv="Content-Type" content="text/html; charset=us-ascii">

</head>

<body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;">

<div>Hi PPL-developers</div>

<div><br>

</div>

<div>I would be glad if you could help me find answers to the following questions:</div>

<div><br>

</div>

<div>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? </div>

<div><br>

</div>

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

 in the user manual I found the following text:</div>

<div><br>

</div>

<img apple-inline="yes" id="4C64B020-EA57-4286-A624-C648B845ED66" height="61" width="326" apple-width="yes" apple-height="yes" src="cid:BC9F6334-FB66-4E2B-BE47-2E4A8D844CD6">

<div><br>

</div>

<div>What are the differences between these two functions? Do they differ in precision? complexity?</div>

<div><br>

</div>

<div>3. What is the function corresponding to poly_hull_assign for Octagon?</div>

<div><br>

</div>

<div>Many thanks in advance</div>

<div>Bishoksan</div>

</body>

</html>