An Abstract Domain to Infer Linear Absolute Value Equalities

The classic linear (technically, affine) equality abstract domain, which can infer linear equality relations among variables of a program automatically, is one of the earliest and fundamental abstract domains. As a lightweight relational abstract domain, it has been widely used in program analysis. However, it cannot express non-convex properties that appear naturally due to the inherent disjuncti...