Pentagons

Abstract

We introduce Pentagons (Pntg), a weakly relational numerical abstract domain useful for the validation of array accesses in byte-code and intermediate languages (IL). This abstract domain captures properties of the form of x ε [a, b]∧x < y. It is more precise than the well known Interval domain, but it is less precise than the Octagon domain.