Abstract interpretation meets convex optimization

作者：Gawlitza Thomas Martin^*; Seidl Helmut; Adje Assale; Gaubert Stephane; Goubault Eric

来源：Journal of Symbolic Computation, 2012, 47(12): 1416-1446.

DOI：10.1016/j.jsc.2011.12.048

• Static analysis
• Abstract interpretation
• Fixpoint equations
• Convex optimization
• Strategy improvement algorithms
• Semi-definite relaxation

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 ascending chains. In order to enforce termination within the abstract interpretation framework, a widening/narrowing approach can be applied that trades the guarantee of termination against a potential loss of precision. Alternatively, recently strategy improvement algorithms have been proposed for computing numerical invariants which do not suffer the imprecision incurred by widenings. Before, strategy improvement algorithms have successfully been applied for solving two-players zero-sum games. In this article we discuss and compare max-strategy and min-strategy improvement algorithms for static program analysis. For that, the algorithms are cast within a common general framework of solving systems of fixpoint equations x = e where the right-hand sides e are maxima of finitely many monotone and concave functions. Then we indicate how the general setting can be instantiated for inferring numerical invariants of programs based on non-linear templates.

• 出版日期2012-12
• 单位中国地震局; INRIA