# Automatic Repair of Overflowing Expressions with Abstract Interpretation

arXiv: https://arxiv.org/abs/1309.5148 · HTML: https://mlsanity.com/paper/1309.5148/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 20 Sep 2013.

## Built on by (most cited first, 1 of 1)

- [Repairing Group-Level Errors for DNNs Using Weighted Regularization](https://mlsanity.com/paper/2203.13612/) (2022)

## Abstract (arXiv)

We consider the problem of synthesizing provably non-overflowing integer arithmetic expressions or Boolean relations among integer arithmetic expressions. First we use a numerical abstract domain to infer numerical properties among program variables. Then we check if those properties guarantee that a given expression does not overflow. If this is not the case, we synthesize an equivalent, yet not-overflowing expression, or we report that such an expression does not exists. The synthesis of a non-overflowing expression depends on three, orthogonal factors: the input expression (e.g., is it linear, polynomial,... ?), the output expression (e.g., are case splits allowed?), and the underlying numerical abstract domain - the more precise the abstract domain is, the more correct expressions can be synthesized. We consider three common cases: (i) linear expressions with integer coefficients and intervals; (ii) Boolean expressions of linear expressions; and (iii) linear expressions with templates. In the first case we prove there exists a complete and polynomial algorithm to solve the problem. In the second case, we have an incomplete yet polynomial algorithm, whereas in the third we have a complete yet worst-case exponential algorithm.