Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis
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 quadra...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2012-01-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/687/pdf |
| _version_ | 1797268711303806976 |
|---|---|
| author | Assalé Adjé Stéphane Gaubert Eric Goubault |
| author_facet | Assalé Adjé Stéphane Gaubert Eric Goubault |
| author_sort | Assalé Adjé |
| collection | DOAJ |
| description | 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). |
| first_indexed | 2024-04-25T01:36:49Z |
| format | Article |
| id | doaj.art-9fdf31bf6ead4b6fbfae087ae8d8d8a3 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:36:49Z |
| publishDate | 2012-01-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-9fdf31bf6ead4b6fbfae087ae8d8d8a32024-03-08T09:27:54ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742012-01-01Volume 8, Issue 110.2168/LMCS-8(1:1)2012687Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysisAssalé AdjéStéphane GaubertEric GoubaultWe 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://lmcs.episciences.org/687/pdfcomputer science - logic in computer sciencemathematics - optimization and control |
| spellingShingle | Assalé Adjé Stéphane Gaubert Eric Goubault Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis Logical Methods in Computer Science computer science - logic in computer science mathematics - optimization and control |
| title | Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis |
| title_full | Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis |
| title_fullStr | Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis |
| title_full_unstemmed | Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis |
| title_short | Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis |
| title_sort | coupling policy iteration with semi definite relaxation to compute accurate numerical invariants in static analysis |
| topic | computer science - logic in computer science mathematics - optimization and control |
| url | https://lmcs.episciences.org/687/pdf |
| work_keys_str_mv | AT assaleadje couplingpolicyiterationwithsemidefiniterelaxationtocomputeaccuratenumericalinvariantsinstaticanalysis AT stephanegaubert couplingpolicyiterationwithsemidefiniterelaxationtocomputeaccuratenumericalinvariantsinstaticanalysis AT ericgoubault couplingpolicyiterationwithsemidefiniterelaxationtocomputeaccuratenumericalinvariantsinstaticanalysis |