HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
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 Connect in order to contact the contributor
Submitted on : Wednesday, January 3, 2018 - 12:12:49 AM
Last modification on : Friday, February 4, 2022 - 3:09:35 AM

Identifiers

Collections

CNRS | LIX | CMAP | X-CMAP | X-LIX | INRIA | X | UNIV-PARIS-SACLAY | X-DEP-MATHA | X-DEP-INFO | GS-COMPUTER-SCIENCE | INRIA2

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 Datacite

Share

Metrics

Record views

147

 

Contact                    Legal Notice                    Personal Data