Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis

A. Adjé 1 Stéphane Gaubert 2, 3 E. Goubault 4
3 MAXPLUS - Max-plus algebras and mathematics of decision
CMAP - Centre de Mathématiques Appliquées - Ecole Polytechnique, Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR
4 LMeASI - Laboratoire Modélisation et Analyse de Systèmes en Interaction
LIST - Laboratoire d'Intégration des Systèmes et des Technologies : DRT/LIST
Abstract : We introduce a new domain for finding precise numerical invariants of pro- grams by abstract interpretation. This domain, which consists of sub-level sets of non- linear functions, generalizes the domain of linear templates introduced by Manna, Sankara- narayanan, and Sipma. In the case of quadratic templates, we use Shor's semi-definite relaxation to derive safe and computable abstractions of semantic functionals, and we show that the abstract fixpoint can be over-approximated by coupling policy iteration and semi-definite programming. We demonstrate the interest of our approach on a series of examples (filters, integration schemes) including a degenerate one (symplectic scheme).
Type de document :
Article dans une revue
Log. Methods Comput. Sci., Institute of Theoretical Computer Science of the Technische Universität Braunschweig, 2012, 8 (1), pp.1:01, 32. 〈10.2168/LMCS-8(1:1)2012〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00782742
Contributeur : Canimogy Cogoulane <>
Soumis le : mercredi 30 janvier 2013 - 15:06:40
Dernière modification le : lundi 24 septembre 2018 - 11:34:02

Lien texte intégral

Identifiants

Collections

Citation

A. Adjé, Stéphane Gaubert, E. Goubault. Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis. Log. Methods Comput. Sci., Institute of Theoretical Computer Science of the Technische Universität Braunschweig, 2012, 8 (1), pp.1:01, 32. 〈10.2168/LMCS-8(1:1)2012〉. 〈hal-00782742〉

Partager

Métriques

Consultations de la notice

294