Interprocedural analyses: a comparison
Identifieur interne : 002336 ( Main/Merge ); précédent : 002335; suivant : 002337Interprocedural analyses: a comparison
Auteurs : H. Seidl [Allemagne] ; C. FechtSource :
- 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.
Links toward previous steps (curation, corpus...)
- to stream PascalFrancis, to step Corpus: 000F40
- to stream PascalFrancis, to step Curation: 000029
- to stream PascalFrancis, to step Checkpoint: 000C90
Links to Exploration step
Pascal:00-0246834Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Interprocedural analyses: a comparison</title><author><name sortKey="Seidl, H" sort="Seidl, H" uniqKey="Seidl H" first="H." last="Seidl">H. Seidl</name><affiliation wicri:level="1"><inist:fA14 i1="01"><s1>Universitaet Trier</s1><s2>Trier</s2><s3>DEU</s3><sZ>1 aut.</sZ></inist:fA14><country>Allemagne</country><wicri:noRegion>Trier</wicri:noRegion><wicri:noRegion>Universitaet Trier</wicri:noRegion><wicri:noRegion>Universitaet Trier</wicri:noRegion></affiliation></author><author><name sortKey="Fecht, C" sort="Fecht, C" uniqKey="Fecht C" first="C." last="Fecht">C. Fecht</name></author></titleStmt><publicationStmt><idno type="wicri:source">INIST</idno><idno type="inist">00-0246834</idno><date when="2000">2000</date><idno type="stanalyst">PASCAL 00-0246834 EI</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></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Interprocedural analyses: a comparison</title><author><name sortKey="Seidl, H" sort="Seidl, H" uniqKey="Seidl H" first="H." last="Seidl">H. Seidl</name><affiliation wicri:level="1"><inist:fA14 i1="01"><s1>Universitaet Trier</s1><s2>Trier</s2><s3>DEU</s3><sZ>1 aut.</sZ></inist:fA14><country>Allemagne</country><wicri:noRegion>Trier</wicri:noRegion><wicri:noRegion>Universitaet Trier</wicri:noRegion><wicri:noRegion>Universitaet Trier</wicri:noRegion></affiliation></author><author><name sortKey="Fecht, C" sort="Fecht, C" uniqKey="Fecht C" first="C." last="Fecht">C. Fecht</name></author></analytic><series><title level="j" type="main">Journal of Logic Programming</title><title level="j" type="abbreviated">J Logic Program</title><idno type="ISSN">0743-1066</idno><imprint><date when="2000">2000</date></imprint></series></biblStruct></sourceDesc><seriesStmt><title level="j" type="main">Journal of Logic Programming</title><title level="j" type="abbreviated">J Logic Program</title><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>Théorie</term><term>Langage orienté procédure</term><term>Linguistique mathématique</term><term>Programmation logique</term><term>Théorie approximation</term><term>Evaluation fonction</term><term>Théorie automate</term><term>Diagnostic programme</term></keywords></textClass></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></list><tree><noCountry><name sortKey="Fecht, C" sort="Fecht, C" uniqKey="Fecht C" first="C." last="Fecht">C. Fecht</name></noCountry><country name="Allemagne"><noRegion><name sortKey="Seidl, H" sort="Seidl, H" uniqKey="Seidl H" first="H." last="Seidl">H. Seidl</name></noRegion></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Rhénanie/explor/UnivTrevesV1/Data/Main/Merge
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 002336 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 002336 | 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= Merge
|type= RBID
|clé= Pascal:00-0246834
|texte= Interprocedural analyses: a comparison
}}
| This area was generated with Dilib version V0.6.31. |  |