Abstract interpretation with higher-dimensional ellipsoids and conic extrapolation

DOI10.1007/978-3-319-21690-4_24zbMATH Open1381.68178arXiv1509.08700OpenAlexW2130096835MaRDI QIDQ1702927FDOQ1702927

Arnaud J. Venet, Mendes Oulamara

Publication date: 1 March 2018

Abstract: The inference and the verification of numerical relationships among variables of a program is one of the main goals of static analysis. In this paper, we propose an Abstract Interpretation framework based on higher-dimensional ellipsoids to automatically discover symbolic quadratic invariants within loops, using loop counters as implicit parameters. In order to obtain non-trivial invariants, the diameter of the set of values taken by the numerical variables of the program has to evolve (sub-)linearly during loop iterations. These invariants are called ellipsoidal cones and can be seen as an extension of constructs used in the static analysis of digital filters. Semidefinite programming is used to both compute the numerical results of the domain operations and provide proofs (witnesses) of their correctness.

Full work available at URL: https://arxiv.org/abs/1509.08700

zbMATH Keywords

semidefinite programmingstatic analysisellipsoidsconic extrapolation

Mathematics Subject Classification ID

Semidefinite programming (90C22) Computer graphics; computational geometry (digital and algorithmic aspects) (68U05) Specification and verification (program logics, model checking, etc.) (68Q60)

Cited In (3)

• Counterexample- and simulation-guided floating-point loop invariant synthesis
• Validating numerical semidefinite programming solvers for polynomial invariants
• Verification-guided programmatic controller synthesis

This page was built for publication: Abstract interpretation with higher-dimensional ellipsoids and conic extrapolation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1702927)