A framework for precise program analysis in numerical abstract interpretation

Abstract interpretation is a technique for static program analysis that approximates program semantics over abstract domains. This approach computes fixpoints within these domains, providing sound approximations of program behavior without requiring execution. To guarantee termination of fixpoint computations, widening and narrowing operators are traditionally employed. However, these operators often introduce a significant loss of precision compared to widening-free analyses, which may not terminate. In general, the exact abstract semantics cannot be computed on domains with infinite ascending chains. In this thesis, we propose a framework that—by suitably restricting the expressiveness of the programming language and requiring specific properties of the abstract domain—makes it possible to compute abstract semantics exactly. The framework builds on earlier work by Zaninotto and is based on bounding the set of abstract values a program may take. This ensures that whenever a fixpoint computation exceeds the bound, divergence is detected. More concretely, given an abstract domain and a program, we identify a subdomain without infinite ascending chains, while preserving the program's semantics from the original domain. Compared to previous work, this thesis improves the precision of the bounds, enabling more efficient computation. Furthermore, while earlier results were limited to interval semantics, we present a general framework for constructing bounded abstract domains. This framework is parameterized by so-called feature functions, which capture the aspects of abstract elements that are bounded to define the subdomain. We demonstrate the applicability of this approach to both the Interval Domain and the Pure Zone Domain (also known as the Potential Set Abstraction).