Interprocedural analyses: a comparison
Identifieur interne : 001F27 ( Main/Exploration ); précédent : 001F26; suivant : 001F28Interprocedural analyses: a comparison
Auteurs : Helmut Seidl [Allemagne] ; Christian Fecht [Allemagne]Source :
- The Journal of Logic Programming [ 0743-1066 ] ; 2000.
Descripteurs français
- Pascal (Inist)
English descriptors
- KwdEn :
Abstract
We present a framework for program analysis of languages with procedures which is general enough to allow for a comparison of various approaches to interprocedural analysis. Our framework is based on a small-step operational semantics and subsumes both frameworks for imperative and for logic languages. We consider reachability analysis, that is, the problem of approximating the sets of program states reaching program points. We use our framework in order to clarify the impact of several independent design decisions on the precision of the analysis. Thus, we compare intraprocedural forward accumulation with intraprocedural backward accumulation. Furthermore, we consider both relational and functional approaches. While for relational analysis the accumulation strategy makes no difference in precision, we prove for functional analysis that forward accumulation may lose precision against backward accumulation. Concerning the relative precision of relational analyses and corresponding functional analyses, we exhibit scenarios where functional analysis does not lose precision. Finally, we explain why even an enhancement of functional analysis through disjunctive completion of the underlying abstract domain may sometimes lose precision against relational analysis.
Url:
DOI: 10.1016/S0743-1066(99)00058-8
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 001663
- to stream Istex, to step Curation: 001551
- to stream Istex, to step Checkpoint: 000C64
- to stream Main, to step Merge: 002240
- to stream PascalFrancis, to step Corpus: 000F40
- to stream PascalFrancis, to step Curation: 000029
- to stream PascalFrancis, to step Checkpoint: 000C90
- to stream Main, to step Merge: 002336
- to stream Main, to step Curation: 001F27
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title>Interprocedural analyses: a comparison</title><author><name sortKey="Seidl, Helmut" sort="Seidl, Helmut" uniqKey="Seidl H" first="Helmut" last="Seidl">Helmut Seidl</name></author><author><name sortKey="Fecht, Christian" sort="Fecht, Christian" uniqKey="Fecht C" first="Christian" last="Fecht">Christian Fecht</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:9BEE7C26B5A58B6EB1657DE6FE82128ADA3F9802</idno><date when="2000" year="2000">2000</date><idno type="doi">10.1016/S0743-1066(99)00058-8</idno><idno type="url">https://api.istex.fr/document/9BEE7C26B5A58B6EB1657DE6FE82128ADA3F9802/fulltext/pdf</idno><idno type="wicri:Area/Istex/Corpus">001663</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001663</idno><idno type="wicri:Area/Istex/Curation">001551</idno><idno type="wicri:Area/Istex/Checkpoint">000C64</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000C64</idno><idno type="wicri:doubleKey">0743-1066:2000:Seidl H:interprocedural:analyses:a</idno><idno type="wicri:Area/Main/Merge">002240</idno><idno type="wicri:source">INIST</idno><idno type="RBID">Pascal:00-0246834</idno><idno type="wicri:Area/PascalFrancis/Corpus">000F40</idno><idno type="wicri:Area/PascalFrancis/Curation">000029</idno><idno type="wicri:Area/PascalFrancis/Checkpoint">000C90</idno><idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000C90</idno><idno type="wicri:doubleKey">0743-1066:2000:Seidl H:interprocedural:analyses:a</idno><idno type="wicri:Area/Main/Merge">002336</idno><idno type="wicri:Area/Main/Curation">001F27</idno><idno type="wicri:Area/Main/Exploration">001F27</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a">Interprocedural analyses: a comparison</title><author><name sortKey="Seidl, Helmut" sort="Seidl, Helmut" uniqKey="Seidl H" first="Helmut" last="Seidl">Helmut Seidl</name><affiliation wicri:level="1"><country xml:lang="fr">Allemagne</country><wicri:regionArea>FB IV – Informatik, Universität Trier, D-54286 Trier</wicri:regionArea><wicri:noRegion>54286 Trier</wicri:noRegion><wicri:noRegion>D-54286 Trier</wicri:noRegion></affiliation><affiliation></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Allemagne</country></affiliation></author><author><name sortKey="Fecht, Christian" sort="Fecht, Christian" uniqKey="Fecht C" first="Christian" last="Fecht">Christian Fecht</name><affiliation wicri:level="3"><country xml:lang="fr">Allemagne</country><wicri:regionArea>Universität des Saarlandes, Postfach 151150, D-66041 Saarbrücken</wicri:regionArea><placeName><region type="land" nuts="2">Sarre (Land)</region><settlement type="city">Sarrebruck</settlement></placeName></affiliation></author></analytic><monogr></monogr><series><title level="j">The Journal of Logic Programming</title><title level="j" type="abbrev">JLP</title><idno type="ISSN">0743-1066</idno><imprint><publisher>ELSEVIER</publisher><date type="published" when="2000">2000</date><biblScope unit="volume">43</biblScope><biblScope unit="issue">2</biblScope><biblScope unit="page" from="123">123</biblScope><biblScope unit="page" to="156">156</biblScope></imprint><idno type="ISSN">0743-1066</idno></series><idno type="istex">9BEE7C26B5A58B6EB1657DE6FE82128ADA3F9802</idno><idno type="DOI">10.1016/S0743-1066(99)00058-8</idno><idno type="PII">S0743-1066(99)00058-8</idno></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0743-1066</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Approximation theory</term><term>Automata theory</term><term>Coincidence theorems</term><term>Computational linguistics</term><term>Function evaluation</term><term>Interprocedural analysis</term><term>Logic programming</term><term>Procedure oriented languages</term><term>Program diagnostics</term><term>Pushdown automata</term><term>Reachability analysis</term><term>Relational analysis</term><term>Theory</term></keywords><keywords scheme="Pascal" xml:lang="fr"><term>Diagnostic programme</term><term>Evaluation fonction</term><term>Langage orienté procédure</term><term>Linguistique mathématique</term><term>Programmation logique</term><term>Théorie</term><term>Théorie approximation</term><term>Théorie automate</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">We present a framework for program analysis of languages with procedures which is general enough to allow for a comparison of various approaches to interprocedural analysis. Our framework is based on a small-step operational semantics and subsumes both frameworks for imperative and for logic languages. We consider reachability analysis, that is, the problem of approximating the sets of program states reaching program points. We use our framework in order to clarify the impact of several independent design decisions on the precision of the analysis. Thus, we compare intraprocedural forward accumulation with intraprocedural backward accumulation. Furthermore, we consider both relational and functional approaches. While for relational analysis the accumulation strategy makes no difference in precision, we prove for functional analysis that forward accumulation may lose precision against backward accumulation. Concerning the relative precision of relational analyses and corresponding functional analyses, we exhibit scenarios where functional analysis does not lose precision. Finally, we explain why even an enhancement of functional analysis through disjunctive completion of the underlying abstract domain may sometimes lose precision against relational analysis.</div></front></TEI><affiliations><list><country><li>Allemagne</li></country><region><li>Sarre (Land)</li></region><settlement><li>Sarrebruck</li></settlement></list><tree><country name="Allemagne"><noRegion><name sortKey="Seidl, Helmut" sort="Seidl, Helmut" uniqKey="Seidl H" first="Helmut" last="Seidl">Helmut Seidl</name></noRegion><name sortKey="Fecht, Christian" sort="Fecht, Christian" uniqKey="Fecht C" first="Christian" last="Fecht">Christian Fecht</name><name sortKey="Seidl, Helmut" sort="Seidl, Helmut" uniqKey="Seidl H" first="Helmut" last="Seidl">Helmut Seidl</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Rhénanie/explor/UnivTrevesV1/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001F27 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 001F27 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Rhénanie
|area= UnivTrevesV1
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:9BEE7C26B5A58B6EB1657DE6FE82128ADA3F9802
|texte= Interprocedural analyses: a comparison
}}
| This area was generated with Dilib version V0.6.31. |  |