The polyhedral domain is a powerful and natural domain for program analysis and verification. However, the exponential complexity of polyhedral operations is a key bottleneck in its application. In this talk, we present techniques for building efficient polyhedra-based domains for the verification array accesses in systems code by developing efficiently computable relaxations of the standard convex hull and image computation operations.