Inferring linear invariants with parallelotopes

We propose a new numerical abstract domain for inferring linear invariants based on parallelotopes. The domain may encode any linear constraint, as the polyhedra abstract domain, while maintaining the efficiency of weakly relational abstract domains, such as intervals and octagons. We provide the full set of abstract operators, define a reduced product with intervals and present an experimental comparison with polyhedra and octagons. According to these experiments, the reduced product we propose is much more precise than both polyhedra and octagons in inferring interval constraints.