Zonotopes are a convenient abstract domain for the precise analysis of programs with numerical variables. Compared to the domain of convex polyhedra, it is less expensive and may easily handle non-linear assignments. However, the classical join operator of this abstract domain does not always preserve linear invariants, unlike the convex hull. We present a global join operator that preserves some affine relations. We end up by showing some experiments conducted on the constrained Taylor1+ domain of Apron. © 2012 Elsevier B.V.
Goubault, E., Le Gall, T., & Putot, S. (2012). An accurate join for zonotopes, preserving affine input/output relations. In Electronic Notes in Theoretical Computer Science (Vol. 287, pp. 65–76). https://doi.org/10.1016/j.entcs.2012.09.007