The Omega Project

The Omega project at the University of Maryland developed theories, software and tools for analyzing sets of affine constraints over integer variables. As we have explored more difficult issues in analysis and transformation of scientific programs, we have extended the Omega test to the point where it is a complete system for simplifying and verifying Presburger formulas (Presburger formulas contain affine constraints, the usual logical connectives, and universal and existential quantifiers.
These techniques were originally developed for analyzing programs performing computation science to help determine how to efficiently execute those programs on supercomputers. However, the techniques have proven to be more generally useful and have found uses in applications such as software verification and cache miss analysis.