Skip to Main content Skip to Navigation
Journal articles

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
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).
Document type :
Journal articles
Complete list of metadata

https://hal.inria.fr/hal-00782742
Contributor : Canimogy Cogoulane <>
Submitted on : Wednesday, January 30, 2013 - 3:06:40 PM
Last modification on : Friday, June 25, 2021 - 9:48:02 AM

Links full text

Identifiers

Citation

A. Adjé, Stéphane Gaubert, E. Goubault. Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2012, 8 (1), pp.1:01, 32. ⟨10.2168/LMCS-8(1:1)2012⟩. ⟨hal-00782742⟩

Share

Metrics

Record views

436