Abstract Interpretation with Higher-Dimensional Ellipsoids and Conic Extrapolation
Identifieur interne : 000191 ( Main/Exploration ); précédent : 000190; suivant : 000192Abstract Interpretation with Higher-Dimensional Ellipsoids and Conic Extrapolation
Auteurs : Mendes Oulamara [France] ; Arnaud Venet [États-Unis]Source :
English descriptors
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.
Url:
DOI: 10.1007/978-3-319-21690-4_24
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Hal, to step Corpus: 000058
- to stream Hal, to step Curation: 000058
- to stream Hal, to step Checkpoint: 000152
- to stream Main, to step Merge: 000191
- to stream Main, to step Curation: 000191
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">Abstract Interpretation with Higher-Dimensional Ellipsoids and Conic Extrapolation</title><author><name sortKey="Oulamara, Mendes" sort="Oulamara, Mendes" uniqKey="Oulamara M" first="Mendes" last="Oulamara">Mendes Oulamara</name><affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-59704" status="VALID"> <orgName>École normale supérieure - Paris</orgName> <orgName type="acronym">ENS Paris</orgName> <desc> <address> <addrLine>45, Rue d'Ulm - 75230 Paris cedex 05</addrLine> <country key="FR"></country> </address> <ref type="url">http://www.ens.fr</ref> </desc> </hal:affiliation><country>France</country></affiliation></author><author><name sortKey="Venet, Arnaud" sort="Venet, Arnaud" uniqKey="Venet A" first="Arnaud" last="Venet">Arnaud Venet</name><affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-81793" status="VALID"> <orgName>NASA Ames Research Center</orgName> <orgName type="acronym">ARC</orgName> <desc> <address> <addrLine>Moffett Field, California 94035</addrLine> <country key="US"></country> </address> <ref type="url">http://www.nasa.gov/centers/ames/home/index.html</ref> </desc> </hal:affiliation><country>États-Unis</country></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">HAL</idno><idno type="RBID">Hal:hal-01202346</idno><idno type="halId">hal-01202346</idno><idno type="halUri">https://hal.archives-ouvertes.fr/hal-01202346</idno><idno type="url">https://hal.archives-ouvertes.fr/hal-01202346</idno><idno type="doi">10.1007/978-3-319-21690-4_24</idno><date when="2015-07-18">2015-07-18</date><idno type="wicri:Area/Hal/Corpus">000058</idno><idno type="wicri:Area/Hal/Curation">000058</idno><idno type="wicri:Area/Hal/Checkpoint">000152</idno><idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">000152</idno><idno type="wicri:Area/Main/Merge">000191</idno><idno type="wicri:Area/Main/Curation">000191</idno><idno type="wicri:Area/Main/Exploration">000191</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Abstract Interpretation with Higher-Dimensional Ellipsoids and Conic Extrapolation</title><author><name sortKey="Oulamara, Mendes" sort="Oulamara, Mendes" uniqKey="Oulamara M" first="Mendes" last="Oulamara">Mendes Oulamara</name><affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-59704" status="VALID"> <orgName>École normale supérieure - Paris</orgName> <orgName type="acronym">ENS Paris</orgName> <desc> <address> <addrLine>45, Rue d'Ulm - 75230 Paris cedex 05</addrLine> <country key="FR"></country> </address> <ref type="url">http://www.ens.fr</ref> </desc> </hal:affiliation><country>France</country></affiliation></author><author><name sortKey="Venet, Arnaud" sort="Venet, Arnaud" uniqKey="Venet A" first="Arnaud" last="Venet">Arnaud Venet</name><affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-81793" status="VALID"> <orgName>NASA Ames Research Center</orgName> <orgName type="acronym">ARC</orgName> <desc> <address> <addrLine>Moffett Field, California 94035</addrLine> <country key="US"></country> </address> <ref type="url">http://www.nasa.gov/centers/ames/home/index.html</ref> </desc> </hal:affiliation><country>États-Unis</country></affiliation></author></analytic><idno type="DOI">10.1007/978-3-319-21690-4_24</idno></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="mix" xml:lang="en"><term>conic extrapolation</term><term>ellipsoids</term><term>semidefinite programming</term><term>static analysis</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">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.</div></front></TEI><affiliations><list><country><li>France</li><li>États-Unis</li></country></list><tree><country name="France"><noRegion><name sortKey="Oulamara, Mendes" sort="Oulamara, Mendes" uniqKey="Oulamara M" first="Mendes" last="Oulamara">Mendes Oulamara</name></noRegion></country><country name="États-Unis"><noRegion><name sortKey="Venet, Arnaud" sort="Venet, Arnaud" uniqKey="Venet A" first="Arnaud" last="Venet">Arnaud Venet</name></noRegion></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Amérique/explor/PittsburghV1/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000191 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 000191 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Amérique
|area= PittsburghV1
|flux= Main
|étape= Exploration
|type= RBID
|clé= Hal:hal-01202346
|texte= Abstract Interpretation with Higher-Dimensional Ellipsoids and Conic Extrapolation
}}
| This area was generated with Dilib version V0.6.38. |  |