Tightened Transitive Closure of Integer Addition Constraints

10 years 10 months ago
Tightened Transitive Closure of Integer Addition Constraints
We present algorithms for testing the satisfiability and finding the tightened transitive closure of conjunctions of addition constraints of the form ±x ± y ≤ d and bound constraints of the form ±x ≤ d where x and y are integer variables and d is an integer constrant. The running time of these algorithms is a cubic polynomial in the number of input constraints. We also describe an efficient matrix representation of addition and bound constraints. The matrix representation provides a easy, algebraic implementation of the satisfiability and tightened transitive closure algorithms. We also outline the use of these algorithms for the improved implementation of abstract interpretation methods based on the octagonal abstract domain.
Peter Z. Revesz
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where SARA
Authors Peter Z. Revesz
Comments (0)