Abstract interpretation meets convex optimization. Submitted to Journal Symbolic of Computation

Abstract. Numerical static program analyses by abstract interpretation, e.g., the problem of inferring bounds for the values of numerical program variables, are faced with the problem that the abstract domains often contain infinite ascend-ing chains. In oder to nevertheless enforce termination one traditionally applies a widening/narrowing approach that buys the guarantee for termination for loss of precision. However, recently, several interesting alternative approaches for com-puting numerical invariants by abstract interpretation were developed that aim at higher precision. One interesting research direction in this context is the study of strategy improvement algorithms. Such algorithms are successfully applied for solving two-players zero-sum games. In the present paper we discuss and com-pare max-strategy and min-strategy improvement algorithms that in particular can be utilized for computing numerical invariants by abstract interpretation. Our goal is to provide the intuitions behind these approaches by focussing on a particular application, namely template-based numerical analysis.