Widening Operators for Weakly-Relational Numeric Abstractions (Extended Abstract)

TL;DR

This paper addresses divergence issues in extrapolation operators for weakly-relational numeric domains and proposes algorithms to eliminate redundant constraints, improving the reliability of these abstractions.

Contribution

It identifies the cause of divergence problems and introduces algorithms to eliminate redundant constraints, enhancing the stability of weakly-relational numeric abstractions.

Findings

Divergence issues are caused by redundant constraints.

Algorithms can effectively eliminate redundancy.

Improved stability of numeric abstractions.

Abstract

We discuss the divergence problems recently identified in some extrapolation operators for weakly-relational numeric domains. We identify the cause of the divergences and point out that resorting to more concrete, syntactic domains can be avoided by researching suitable algorithms for the elimination of redundant constraints in the chosen representation.