A Geometric Local Quantifier-Elimination Heuristic for Octagonal Constraints

will be then used to apply to the case where program properties are
expressed using weakly relational numerical  properties of the form
($l \le \pm x \pm y \le h$), also called octagonal constraints. It will
be shown that an efficient heuristic (quadratic in the number of variables)
can  be developed using local geometric techniques for incomplete
quantifier elimination from verification conditions expressed using
octagonal constraints.
The quality (strength) of invariants generated using the incomplete
quantifier elimination heuristic appears to be adequate (in comparison
with invariants generated by the Interproc tool); however, this issue is
being further investigated.

This is joint work with Hengjun Zhao of the Chinese Academy of
Sciences and Zhihai Zhang of the Peking University.