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 <>
Submitted on : Wednesday, January 3, 2018 - 12:12:49 AM
Last modification on : Wednesday, May 27, 2020 - 12:20:03 PM

Identifiers

Collections

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

295