Skip to Main content Skip to Navigation
Journal articles

A Fast Method to Compute Disjunctive Quadratic Invariants of Numerical Programs

Xavier Allamigeon 1, 2 Stéphane Gaubert 1, 2 Eric Goubault 3 Sylvie Putot 3 Nikolas Stott 2, 1
1 TROPICAL - TROPICAL
CMAP - Centre de Mathématiques Appliquées - Ecole Polytechnique, Inria Saclay - Ile de France
2 CMAP - Centre de Mathématiques Appliquées - Ecole Polytechnique
3 LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
Abstract : We introduce a new method to compute non-convex invariants of numerical programs, which includes the class of switched affine systems with affine guards. We obtain disjunctive and non-convex invariants by associating different partial execution traces with different ellipsoids. A key ingredient is the solution of non-monotone fixed points problems over the space of ellipsoids with a reduction to small size linear matrix inequalities. This allows us to analyze instances that are inaccessible in terms of expressivity or scale by earlier methods based on semi-definite programming.
Document type :
Journal articles
Complete list of metadata
https://hal.inria.fr/hal-01674495
Contributor : Stephane Gaubert <>
Submitted on : Wednesday, January 3, 2018 - 12:12:49 AM
Last modification on : Wednesday, May 27, 2020 - 12:20:03 PM

Identifiers

Collections

CNRS | LIX | CMAP | X-CMAP | X-LIX | INRIA | X | X-DEP-MATHA | X-DEP-INFO

Citation

Xavier Allamigeon, Stéphane Gaubert, Eric Goubault, Sylvie Putot, Nikolas Stott. A Fast Method to Compute Disjunctive Quadratic Invariants of Numerical Programs. ACM Transactions on Embedded Computing Systems (TECS), ACM, 2017, Special Issue ESWEEK 2017, CASES 2017, CODES + ISSS 2017 and EMSOFT 2017, 16 (5s), pp.1-19. ⟨10.1145/3126502⟩. ⟨hal-01674495⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

295

 

Contact                    Legal Notice                    Personal Data