In the theory of abstract interpretation, a descending phase may be used to improve the precision of the analysis after a post-fixpoint has been reached. Termination is often guaranteed by using narrowing operators. This is especially true on numerical domains, since they are generally endowed with infinite descending chains which may lead to a non-terminating descending phase in the absence of narrowing. We provide an abstract semantics which improves the analysis precision and shows that, for a large class of numerical abstract domains over integer variables (such as intervals, octagons and template polyhedra), it is possible to avoid infinite descending chains and omit narrowing. Moreover, we propose a new family of narrowing operators for real variables which improves the analysis precision.
展开▼
