Abstractions of Sequences, Functions and Operators

TL;DR

This paper develops new theoretical frameworks and practical tools for abstracting and analyzing recursive and complex numerical functions using lattice theory and Galois connections, with applications in program analysis and hybrid systems.

Contribution

It introduces B-bound domains for non-linear function invariants and a domain abstraction functor for lifting mappings to function space, advancing higher-order abstract interpretation.

Findings

B-bound domains enable inferring non-linear invariants.

Convexity property simplifies transfer function design.

Domain abstraction supports symbolic to numerical function transition.

Abstract

We present theoretical and practical results on the order theory of lattices of functions, focusing on Galois connections that abstract (sets of) functions - a topic known as higher-order abstract interpretation. We are motivated by the challenge of inferring closed-form bounds on functions which are defined recursively, i.e. as the fixed point of an operator or, equivalently, as the solution to a functional equation. This has multiple applications in program analysis (e.g. cost analysis, loop acceleration, declarative language analysis) and in hybrid systems governed by differential equations. Our main contribution is a new family of constraint-based abstract domains for abstracting numerical functions, B-bound domains, which abstract a function f by a conjunction of bounds from a preselected set of boundary functions. They allow inferring highly non-linear numerical invariants, which classical numerical abstract domains struggle with. We uncover a convexity property in the constraint space that simplifies, and, in some cases, fully automates, transfer function design. We also introduce domain abstraction, a functor that lifts arbitrary mappings in value space to Galois connections in function space. This supports abstraction from symbolic to numerical functions (i.e. size abstraction), and enables dimensionality reduction of equations. We base our constructions of transfer functions on a simple operator language, starting with sequences, and extending to more general functions, including multivariate, piecewise, and non-discrete domains.