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

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

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⟩

Share

Metrics

Record views

147