A Fast Method to Compute Disjunctive Quadratic Invariants of Numerical Programs

作者：Allamigeon Xavier^*; Gaubert Stephane; Goubault Eric; Putot Sylvie; Stott Nikolas

来源：ACM Transactions on Embedded Computing Systems, 2017, 16(5s): 166.

DOI：10.1145/3126502

• Static analysis
• abstract interpretation
• invariant generation
• stability
• hybrid and switched linear systems

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.

• 出版日期2017-10
• 单位INRIA