Octagonal constraints expressing weakly relational numerical properties of the form (l ≤ ± x ± y ≤ h) have been found useful and effective in static analysis of numerical programs. Their analysis serves as a key component of the tool ASTREE based on abstract interpretation framework proposed by Patrick Cousot and his group, which has been successfully used to analyze commercial software consisting of hundreds of thousand of lines of code. This talk will discuss a heuristic based on the quantifier-elimination (QE) approach presented by Kapur (2005) that can be used to automatically derive loop invariants expressed as a conjunction of octagonal constraints in O(n²), where n is the number of program variables over which these constraints are expressed. This is in contrast to the algorithms developed in Mine’s thesis which have the complexity at least O(n³). The restricted QE heuristic usually generates invariants stronger than those obtained by the freely available Interproc tool. Extensions of the proposed approach to generating disjunctive invariants will be presented.