We propose a modular inference mechanism, based on an advanced type system with Presburger arithmetic, to help identify array checks that can be safely eliminated. Our proposal works for a core imperative language with assignments, and can discover symbolic program states (or postconditions) to support the elimination of redundant checks. Our inference is modular as it is able to process each method independently, and yet exploit the different contexts of its multiple callers. We achieve this by converting each partially-safe check into a precondition that is propagated up its callers' sites for further inference. This approach provides for a highly accurate interprocedural optimization. The results of our modular inference can be used by a program specialization phase that can maximise the elimination of safe checks. We have implemented a prototype inference system and have also proven its soundness. Initial experiments suggest that such an inference system can be both accurate and scalable.