Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis

Assalé Adjé; Stéphane Gaubert; Eric Goubault

doi:10.2168/LMCS-8(1:1)2012

Assalé Adjé ; Stéphane Gaubert ; Eric Goubault - Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis

lmcs:687 - Logical Methods in Computer Science, January 19, 2012, Volume 8, Issue 1 - https://doi.org/10.2168/LMCS-8(1:1)2012

Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysisArticle

Authors: Assalé Adjé ; Stéphane Gaubert ; Eric Goubault

We introduce a new domain for finding precise numerical invariants of programs by abstract interpretation. This domain, which consists of level sets of non-linear functions, generalizes the domain of linear "templates" introduced by Manna, Sankaranarayanan, and Sipma. In the case of quadratic templates, we use Shor's semi-definite relaxation to derive computable yet precise abstractions of semantic functionals, and we show that the abstract fixpoint equation can be solved accurately by coupling policy iteration and semi-definite programming. We demonstrate the interest of our approach on a series of examples (filters, integration schemes) including a degenerate one (symplectic scheme).

https://doi.org/10.2168/LMCS-8(1:1)2012

Source: arXiv.org:1111.5223

Volume: Volume 8, Issue 1

Published on: January 19, 2012

Imported on: June 11, 2010

Keywords: Computer Science - Logic in Computer Science,Mathematics - Optimization and Control

Licence: arXiv.org - Non-exclusive license to distribute

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

14 Documents citing this article

Hongming Liu;Hongfei Fu;Zhiyong Yu;Jiaxin Song;Guoqiang Li, 2022, Scalable linear invariant generation with Farkas’ lemma, Proceedings of the ACM on Programming Languages, 6, OOPSLA2, pp. 204-232, 10.1145/3563295, https://doi.org/10.1145/3563295.

Yucheng Ji;Hongfei Fu;Bin Fang;Haibo Chen, Lecture notes in computer science, Affine Loop Invariant Generation via Matrix Algebra, pp. 257-281, 2022, 10.1007/978-3-031-13185-1_13, https://doi.org/10.1007/978-3-031-13185-1_13.

Anastasiia Izycheva;Eva Darulova;Helmut Seidl, Lecture notes in computer science, Counterexample- and Simulation-Guided Floating-Point Loop Invariant Synthesis, pp. 156-177, 2020, 10.1007/978-3-030-65474-0_8, https://doi.org/10.1007/978-3-030-65474-0_8.

Asma Mansouri;Matthieu Martel;Oana Silvia Serea, 2022 8th International Conference on Control, Decision and Information Technologies (CoDIT), Fixed Point Computation by Exponentiating Linear Operators, pp. 1096-1102, 2019, Paris, France, 10.1109/codit.2019.8820696.

Assalé Adjé, Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, Coupling Policy Iterations with Piecewise Quadratic Lyapunov Functions, pp. 143-152, 2017, Pittsburgh Pennsylvania USA, 10.1145/3049797.3049825.

Assalé Adjé;Pierre-Loïc Garoche;Victor Magron, 2017, A Sums-of-Squares extension of policy iterations, 25, pp. 60-78, 10.1016/j.nahs.2017.03.001, https://hal.archives-ouvertes.fr/hal-01448179.

Sriram Sankaranarayanan;Mohamed Amin Ben Sassi, Lecture notes in computer science, Template Polyhedra with a Twist, pp. 321-341, 2017, 10.1007/978-3-319-66706-5_16.

Steven de Oliveira;Saddek Bensalem;Virgile Prevosto, Zenodo (CERN European Organization for Nuclear Research), Synthesizing Invariants by Solving Solvable Loops, pp. 327-343, 2017, 10.1007/978-3-319-68167-2_22, https://zenodo.org/record/893067.

Xavier Allamigeon;Stéphane Gaubert;Nikolas Stott;Éric Goubault;Sylvie Putot, 2016, A Scalable Algebraic Method to Infer Quadratic Invariants of Switched Systems, ACM Transactions on Embedded Computing Systems, 15, 4, pp. 1-20, 10.1145/2932187.

Assalé Adjé, 2015, Policy Iteration in Finite Templates Domain, Electronic Notes in Theoretical Computer Science, 317, pp. 3-18, 10.1016/j.entcs.2015.10.002, https://doi.org/10.1016/j.entcs.2015.10.002.

Xavier Allamigeon;Stéphane Gaubert;Eric Goubault;Sylvie Putot;Nikolas Stott, A scalable algebraic method to infer quadratic invariants of switched systems, pp. 75-84, 2015, Amsterdam, Netherlands, 10.1109/emsoft.2015.7318262.

Victor Magron;Xavier Allamigeon;Stéphane Gaubert;Benjamin Werner, 2014, Certification of real inequalities: templates and sums of squares, arXiv (Cornell University), 151, 2, pp. 477-506, 10.1007/s10107-014-0834-5, https://arxiv.org/abs/1403.5899.

Eric Goubault, Lecture notes in computer science, Static Analysis by Abstract Interpretation of Numerical Programs and Systems, and FLUCTUAT, pp. 1-3, 2013, 10.1007/978-3-642-38856-9_1.

Xavier Allamigeon;Stéphane Gaubert;Victor Magron;Benjamin Werner, arXiv (Cornell University), Certification of Bounds of Non-linear Functions: The Templates Method, pp. 51-65, 2013, 10.1007/978-3-642-39320-4_4, http://arxiv.org/abs/1307.3231.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 1626 times.

This article's PDF has been downloaded 363 times.