Interprocedural analyses: a comparison
Identifieur interne : 000C90 ( PascalFrancis/Checkpoint ); précédent : 000C89; suivant : 000C91Interprocedural 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.
Affiliations:
Links toward previous steps (curation, corpus...)
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></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><inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0743-1066</s0></fA01><fA02 i1="01"><s0>JLPRE2</s0></fA02><fA03 i2="1"><s0>J Logic Program</s0></fA03><fA05><s2>43</s2></fA05><fA06><s2>2</s2></fA06><fA08 i1="01" i2="1" l="ENG"><s1>Interprocedural analyses: a comparison</s1></fA08><fA11 i1="01" i2="1"><s1>SEIDL (H.)</s1></fA11><fA11 i1="02" i2="1"><s1>FECHT (C.)</s1></fA11><fA14 i1="01"><s1>Universitaet Trier</s1><s2>Trier</s2><s3>DEU</s3><sZ>1 aut.</sZ></fA14><fA20><s1>123-156</s1></fA20><fA21><s1>2000</s1></fA21><fA23 i1="01"><s0>ENG</s0></fA23><fA43 i1="01"><s1>INIST</s1><s2>21798</s2></fA43><fA44><s0>A100</s0></fA44><fA45><s0>50 Refs.</s0></fA45><fA47 i1="01" i2="1"><s0>00-0246834</s0></fA47><fA60><s1>P</s1></fA60><fA61><s0>A</s0></fA61><fA64 i1="01" i2="1"><s0>Journal of Logic Programming</s0></fA64><fA66 i1="01"><s0>USA</s0></fA66><fC01 i1="01" l="ENG"><s0>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.</s0></fC01><fC02 i1="01" i2="X"><s0>001D02B03</s0></fC02><fC02 i1="02" i2="X"><s0>001D02B02</s0></fC02><fC02 i1="03" i2="X"><s0>001D02A</s0></fC02><fC02 i1="04" i2="X"><s0>001A02I01</s0></fC02><fC03 i1="01" i2="1" l="ENG"><s0>Interprocedural analysis</s0><s4>INC</s4></fC03><fC03 i1="02" i2="1" l="ENG"><s0>Reachability analysis</s0><s4>INC</s4></fC03><fC03 i1="03" i2="1" l="ENG"><s0>Relational analysis</s0><s4>INC</s4></fC03><fC03 i1="04" i2="1" l="ENG"><s0>Pushdown automata</s0><s4>INC</s4></fC03><fC03 i1="05" i2="1" l="ENG"><s0>Coincidence theorems</s0><s4>INC</s4></fC03><fC03 i1="06" i2="1" l="FRE"><s0>Théorie</s0></fC03><fC03 i1="06" i2="1" l="ENG"><s0>Theory</s0></fC03><fC03 i1="07" i2="1" l="FRE"><s0>Langage orienté procédure</s0></fC03><fC03 i1="07" i2="1" l="ENG"><s0>Procedure oriented languages</s0></fC03><fC03 i1="08" i2="1" l="FRE"><s0>Linguistique mathématique</s0></fC03><fC03 i1="08" i2="1" l="ENG"><s0>Computational linguistics</s0></fC03><fC03 i1="09" i2="1" l="FRE"><s0>Programmation logique</s0></fC03><fC03 i1="09" i2="1" l="ENG"><s0>Logic programming</s0></fC03><fC03 i1="10" i2="1" l="FRE"><s0>Théorie approximation</s0></fC03><fC03 i1="10" i2="1" l="ENG"><s0>Approximation theory</s0></fC03><fC03 i1="11" i2="1" l="FRE"><s0>Evaluation fonction</s0></fC03><fC03 i1="11" i2="1" l="ENG"><s0>Function evaluation</s0></fC03><fC03 i1="12" i2="1" l="FRE"><s0>Théorie automate</s0></fC03><fC03 i1="12" i2="1" l="ENG"><s0>Automata theory</s0></fC03><fC03 i1="13" i2="1" l="FRE"><s0>Diagnostic programme</s0><s3>P</s3></fC03><fC03 i1="13" i2="1" l="ENG"><s0>Program diagnostics</s0><s3>P</s3></fC03><fN21><s1>171</s1></fN21></pA></standard></inist><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/PascalFrancis/Checkpoint
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000C90 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Checkpoint/biblio.hfd -nk 000C90 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Rhénanie
|area= UnivTrevesV1
|flux= PascalFrancis
|étape= Checkpoint
|type= RBID
|clé= Pascal:00-0246834
|texte= Interprocedural analyses: a comparison
}}
| This area was generated with Dilib version V0.6.31. |  |