Numerical Invariants through Convex Relaxation and Max-Strategy Iteration

TL;DR

This paper introduces a max-strategy improvement algorithm for efficiently computing least fixpoints of complex operators, aiding in numerical invariants analysis in program verification.

Contribution

It develops a novel max-strategy improvement method for operators that are maxima of monotone, order-concave functions, with applications to numerical invariants in program analysis.

Findings

Algorithm effectively computes least fixpoints for complex operators.

Application to quadratic templates improves numerical invariants analysis.

Enhances tools for program verification and systems analysis.

Abstract

In this article we develop a max-strategy improvement algorithm for computing least fixpoints of operators on on the reals that are point-wise maxima of finitely many monotone and order-concave operators. Computing the uniquely determined least fixpoint of such operators is a problem that occurs frequently in the context of numerical program/systems verification/analysis. As an example for an application we discuss how our algorithm can be applied to compute numerical invariants of programs by abstract interpretation based on quadratic templates.