Abstract interpretation meets convex optimization

Citations of this article
Mendeley users who have this article in their library.


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. © 2011 Elsevier Ltd.




Gawlitza, T. M., Seidl, H., Adjé, A., Gaubert, S., & Goubault, É. (2012). Abstract interpretation meets convex optimization. Journal of Symbolic Computation, 47(12), 1416–1446. https://doi.org/10.1016/j.jsc.2011.12.048

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free