Interprocedural analyses: a comparison
Identifieur interne : 001663 ( Istex/Corpus ); précédent : 001662; suivant : 001664Interprocedural analyses: a comparison
Auteurs : Helmut Seidl ; Christian FechtSource :
- The Journal of Logic Programming [ 0743-1066 ] ; 2000.
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
Links to Exploration step
ISTEX:9BEE7C26B5A58B6EB1657DE6FE82128ADA3F9802Le 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><affiliation><mods:affiliation>FB IV – Informatik, Universität Trier, D-54286 Trier, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>Corresponding author. Tel.: +49-651-201-2835; fax: +49-651-201-3822</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: seidl@psi.uni-trier.de</mods:affiliation></affiliation></author><author><name sortKey="Fecht, Christian" sort="Fecht, Christian" uniqKey="Fecht C" first="Christian" last="Fecht">Christian Fecht</name><affiliation><mods:affiliation>Universität des Saarlandes, Postfach 151150, D-66041 Saarbrücken, Germany</mods:affiliation></affiliation></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></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><mods:affiliation>FB IV – Informatik, Universität Trier, D-54286 Trier, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>Corresponding author. Tel.: +49-651-201-2835; fax: +49-651-201-3822</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: seidl@psi.uni-trier.de</mods:affiliation></affiliation></author><author><name sortKey="Fecht, Christian" sort="Fecht, Christian" uniqKey="Fecht C" first="Christian" last="Fecht">Christian Fecht</name><affiliation><mods:affiliation>Universität des Saarlandes, Postfach 151150, D-66041 Saarbrücken, Germany</mods:affiliation></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></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><istex><corpusName>elsevier</corpusName><author><json:item><name>Helmut Seidl</name><affiliations><json:string>FB IV – Informatik, Universität Trier, D-54286 Trier, Germany</json:string><json:string>Corresponding author. Tel.: +49-651-201-2835; fax: +49-651-201-3822</json:string><json:string>E-mail: seidl@psi.uni-trier.de</json:string></affiliations></json:item><json:item><name>Christian Fecht</name><affiliations><json:string>Universität des Saarlandes, Postfach 151150, D-66041 Saarbrücken, Germany</json:string></affiliations></json:item></author><subject><json:item><lang><json:string>eng</json:string></lang><value>Interprocedural analysis</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>Pushdown automata</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>OLDT-resolution</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>Coincidence theorems</value></json:item></subject><language><json:string>eng</json:string></language><originalGenre><json:string>Full-length article</json:string></originalGenre><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.</abstract><qualityIndicators><score>7.088</score><pdfVersion>1.2</pdfVersion><pdfPageSize>468 x 680 pts</pdfPageSize><refBibsNative>true</refBibsNative><keywordCount>4</keywordCount><abstractCharCount>1277</abstractCharCount><pdfWordCount>15657</pdfWordCount><pdfCharCount>79083</pdfCharCount><pdfPageCount>34</pdfPageCount><abstractWordCount>174</abstractWordCount></qualityIndicators><title>Interprocedural analyses: a comparison</title><pii><json:string>S0743-1066(99)00058-8</json:string></pii><refBibs><json:item><host><author></author></host></json:item><json:item><host><author></author></host></json:item><json:item><author><json:item><name>F. Bourdoncle</name></json:item></author><host><volume>2</volume><pages><last>435</last><first>407</first></pages><issue>4</issue><author></author><title>Journal of Functional Programming</title></host><title>Abstract interpretation by dynamic partioning</title></json:item><json:item><host><author></author></host></json:item><json:item><author><json:item><name>B. Le Charlier</name></json:item><json:item><name>A. Cortesi</name></json:item><json:item><name>P. Van Hentenryck</name></json:item></author><host><volume>23</volume><pages><last>278</last><first>237</first></pages><issue>3</issue><author></author><title>Journal of Logic Programming</title></host><title>Evaluation of the domain Prop</title></json:item><json:item><host><author></author></host></json:item><json:item><host><author></author></host></json:item><json:item><author><json:item><name>B. Le Charlier</name></json:item><json:item><name>P. Van Hentenryck</name></json:item></author><host><volume>16</volume><pages><last>101</last><first>35</first></pages><issue>1</issue><author></author><title>ACM Transactions of Programming Languages and Systems (TOPLAS)</title></host><title>Experimental evaluation of a generic abstract interpretation algorithm for Prolog</title></json:item><json:item><host><author></author></host></json:item><json:item><author><json:item><name>A. Cortesi</name></json:item><json:item><name>G. Filé</name></json:item><json:item><name>W.H. Winsborough</name></json:item></author><host><volume>27</volume><pages><last>167</last><first>137</first></pages><issue>2</issue><author></author><title>Journal of Logic Programming</title></host><title>Optimal groundness analysis using propositional logic</title></json:item><json:item><host><author></author></host></json:item><json:item><host><author></author></host></json:item><json:item><author><json:item><name>P. Cousot</name></json:item><json:item><name>R. Cousot</name></json:item></author><host><pages><last>277</last><first>237</first></pages><author></author><title>Formal Descriptions of Programming Concepts</title></host><title>Static determination of dynamic properties of recursive programs</title></json:item><json:item><host><author></author></host></json:item><json:item><host><author></author></host></json:item><json:item><host><author></author></host></json:item><json:item><author><json:item><name>E. Villemonte de la Clergerie</name></json:item><json:item><name>F. Barthélemy</name></json:item></author><host><volume>199</volume><pages><last>198</last><first>167</first></pages><issue>1/2</issue><author></author><title>Theoretical Computer Science</title></host><title>Information flow in tabular interpretations for generalized pushdown automata</title></json:item><json:item><host><author></author></host></json:item><json:item><host><author></author></host></json:item><json:item><author><json:item><name>V. Englebert</name></json:item><json:item><name>B. Le Charlier</name></json:item><json:item><name>D. Roland</name></json:item><json:item><name>P. Van Hentenryck</name></json:item></author><host><volume>23</volume><pages><last>459</last><first>419</first></pages><issue>4</issue><author></author><title>Software – Practice and Experience</title></host><title>Generic abstract interpretation algorithms for Prolog: two optimization techniques and their experimental evaluation</title></json:item><json:item><host><author></author></host></json:item><json:item><host><author></author></host></json:item><json:item><host><author></author></host></json:item><json:item><host><author></author></host></json:item><json:item><host><author></author><title>Flow Analysis of Computer Programs</title></host></json:item><json:item><host><author></author></host></json:item><json:item><host><author></author></host></json:item><json:item><host><author></author></host></json:item><json:item><host><author></author></host></json:item><json:item><author><json:item><name>S. Horwitz</name></json:item><json:item><name>T.W. Reps</name></json:item><json:item><name>M. Sagiv</name></json:item></author><host><volume>167</volume><pages><last>170</last><first>131</first></pages><issue>1/2</issue><author></author><title>Theoretical Computer Science</title></host><title>Precise interprocedural dataflow analysis with applications to constant propagation</title></json:item><json:item><author><json:item><name>J. Hughes</name></json:item><json:item><name>J. Launchbury</name></json:item></author><host><volume>22</volume><pages><last>326</last><first>307</first></pages><author></author><title>Science of Computer Programming (SCP)</title></host><title>Reversing abstract interpretations</title></json:item><json:item><author><json:item><name>D. Jacobs</name></json:item><json:item><name>A. Langen</name></json:item></author><host><volume>13</volume><pages><last>314</last><first>291</first></pages><author></author><title>Journal of Logic Programming</title></host><title>Static analysis of logic programs for independent AND parallelism</title></json:item><json:item><host><author></author></host></json:item><json:item><host><author></author></host></json:item><json:item><host><author></author></host></json:item><json:item><author><json:item><name>J. Knoop</name></json:item><json:item><name>O. Rüthing</name></json:item><json:item><name>B. Steffen</name></json:item></author><host><volume>4</volume><pages><last>246</last><first>211</first></pages><author></author><title>Journal of Programming Languages</title></host><title>Towards a tool kit for the automatic generation of interprocedural data flow analyses</title></json:item><json:item><host><author></author></host></json:item><json:item><host><author></author></host></json:item><json:item><host><author></author></host></json:item><json:item><author><json:item><name>K. Marriott</name></json:item><json:item><name>H. Søndergaard</name></json:item></author><host><volume>2</volume><pages><last>196</last><first>181</first></pages><author></author><title>ACM Letters on Programming Languages and Systems (LOPLAS</title></host><title>Precise and efficient groundness analysis for logic programs</title></json:item><json:item><author><json:item><name>K. Marriott</name></json:item><json:item><name>H. Søndergaard</name></json:item><json:item><name>N.D. Jones</name></json:item></author><host><volume>16</volume><pages><last>648</last><first>607</first></pages><issue>3</issue><author></author><title>ACM Transactions of Programming Languages and Systems (TOPLAS)</title></host><title>Denotational abstract interpretation of logic programs</title></json:item><json:item><host><author></author></host></json:item><json:item><host><author></author></host></json:item><json:item><host><author></author></host></json:item><json:item><host><author></author></host></json:item><json:item><host><author></author></host></json:item><json:item><host><author></author></host></json:item><json:item><host><author></author></host></json:item><json:item><host><author></author></host></json:item><json:item><host><author></author></host></json:item></refBibs><genre><json:string>research-article</json:string></genre><host><volume>43</volume><pii><json:string>S0743-1066(00)X0051-9</json:string></pii><pages><last>156</last><first>123</first></pages><issn><json:string>0743-1066</json:string></issn><issue>2</issue><genre><json:string>journal</json:string></genre><language><json:string>unknown</json:string></language><title>The Journal of Logic Programming</title><publicationDate>2000</publicationDate></host><categories><wos></wos><scienceMetrix><json:string>applied sciences</json:string><json:string>information & communication technologies</json:string><json:string>computation theory & mathematics</json:string></scienceMetrix></categories><publicationDate>2000</publicationDate><copyrightDate>2000</copyrightDate><doi><json:string>10.1016/S0743-1066(99)00058-8</json:string></doi><id>9BEE7C26B5A58B6EB1657DE6FE82128ADA3F9802</id><score>0.4858864</score><fulltext><json:item><extension>pdf</extension><original>true</original><mimetype>application/pdf</mimetype><uri>https://api.istex.fr/document/9BEE7C26B5A58B6EB1657DE6FE82128ADA3F9802/fulltext/pdf</uri></json:item><json:item><extension>zip</extension><original>false</original><mimetype>application/zip</mimetype><uri>https://api.istex.fr/document/9BEE7C26B5A58B6EB1657DE6FE82128ADA3F9802/fulltext/zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/document/9BEE7C26B5A58B6EB1657DE6FE82128ADA3F9802/fulltext/tei"><teiHeader><fileDesc><titleStmt><title level="a">Interprocedural analyses: a comparison</title></titleStmt><publicationStmt><authority>ISTEX</authority><publisher>ELSEVIER</publisher><availability><p>©2000 Elsevier Science Inc.</p></availability><date>2000</date></publicationStmt><sourceDesc><biblStruct type="inbook"><analytic><title level="a">Interprocedural analyses: a comparison</title><author xml:id="author-1"><persName><forename type="first">Helmut</forename><surname>Seidl</surname></persName><email>seidl@psi.uni-trier.de</email><affiliation>FB IV – Informatik, Universität Trier, D-54286 Trier, Germany</affiliation><affiliation>Corresponding author. Tel.: +49-651-201-2835; fax: +49-651-201-3822</affiliation></author><author xml:id="author-2"><persName><forename type="first">Christian</forename><surname>Fecht</surname></persName><affiliation>Universität des Saarlandes, Postfach 151150, D-66041 Saarbrücken, Germany</affiliation></author></analytic><monogr><title level="j">The Journal of Logic Programming</title><title level="j" type="abbrev">JLP</title><idno type="pISSN">0743-1066</idno><idno type="PII">S0743-1066(00)X0051-9</idno><imprint><publisher>ELSEVIER</publisher><date type="published" when="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></monogr><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></fileDesc><profileDesc><creation><date>2000</date></creation><langUsage><language ident="en">en</language></langUsage><abstract xml:lang="en"><p>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.</p></abstract><textClass><keywords scheme="keyword"><list><head>Keywords</head><item><term>Interprocedural analysis</term></item><item><term>Pushdown automata</term></item><item><term>OLDT-resolution</term></item><item><term>Coincidence theorems</term></item></list></keywords></textClass></profileDesc><revisionDesc><change when="1999-04-30">Modified</change><change when="2000">Published</change></revisionDesc></teiHeader></istex:fulltextTEI><json:item><extension>txt</extension><original>false</original><mimetype>text/plain</mimetype><uri>https://api.istex.fr/document/9BEE7C26B5A58B6EB1657DE6FE82128ADA3F9802/fulltext/txt</uri></json:item></fulltext><metadata><istex:metadataXml wicri:clean="Elsevier, elements deleted: tail"><istex:xmlDeclaration>version="1.0" encoding="utf-8"</istex:xmlDeclaration><istex:docType PUBLIC="-//ES//DTD journal article DTD version 4.5.2//EN//XML" URI="art452.dtd" name="istex:docType"></istex:docType><istex:document><converted-article version="4.5.2" docsubtype="fla"><item-info><jid>JLP</jid><aid>6080</aid><ce:pii>S0743-1066(99)00058-8</ce:pii><ce:doi>10.1016/S0743-1066(99)00058-8</ce:doi><ce:copyright type="full-transfer" year="2000">Elsevier Science Inc.</ce:copyright></item-info><head><ce:title>Interprocedural analyses: a comparison</ce:title><ce:author-group><ce:author><ce:given-name>Helmut</ce:given-name><ce:surname>Seidl</ce:surname><ce:cross-ref refid="AFF1"><ce:sup>a</ce:sup></ce:cross-ref><ce:cross-ref refid="COR1">*</ce:cross-ref><ce:e-address>seidl@psi.uni-trier.de</ce:e-address></ce:author><ce:author><ce:given-name>Christian</ce:given-name><ce:surname>Fecht</ce:surname><ce:cross-ref refid="AFF2"><ce:sup>b</ce:sup></ce:cross-ref></ce:author><ce:affiliation id="AFF1"><ce:label>a</ce:label><ce:textfn>FB IV – Informatik, Universität Trier, D-54286 Trier, Germany</ce:textfn></ce:affiliation><ce:affiliation id="AFF2"><ce:label>b</ce:label><ce:textfn>Universität des Saarlandes, Postfach 151150, D-66041 Saarbrücken, Germany</ce:textfn></ce:affiliation><ce:correspondence id="COR1"><ce:label>*</ce:label><ce:text>Corresponding author. Tel.: +49-651-201-2835; fax: +49-651-201-3822</ce:text></ce:correspondence></ce:author-group><ce:date-received day="18" month="9" year="1997"></ce:date-received><ce:date-revised day="30" month="4" year="1999"></ce:date-revised><ce:date-accepted day="14" month="6" year="1999"></ce:date-accepted><ce:abstract class="author"><ce:section-title>Abstract</ce:section-title><ce:abstract-sec><ce:simple-para>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 <ce:italic>reachability analysis</ce:italic>, 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 <ce:italic>forward accumulation</ce:italic> with intraprocedural <ce:italic>backward accumulation</ce:italic>. Furthermore, we consider both <ce:italic>relational</ce:italic> and <ce:italic>functional</ce:italic> 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.</ce:simple-para></ce:abstract-sec></ce:abstract><ce:keywords class="keyword"><ce:section-title>Keywords</ce:section-title><ce:keyword><ce:text>Interprocedural analysis</ce:text></ce:keyword><ce:keyword><ce:text>Pushdown automata</ce:text></ce:keyword><ce:keyword><ce:text>OLDT-resolution</ce:text></ce:keyword><ce:keyword><ce:text>Coincidence theorems</ce:text></ce:keyword></ce:keywords></head></converted-article></istex:document></istex:metadataXml><mods version="3.6"><titleInfo><title>Interprocedural analyses: a comparison</title></titleInfo><titleInfo type="alternative" contentType="CDATA"><title>Interprocedural analyses: a comparison</title></titleInfo><name type="personal"><namePart type="given">Helmut</namePart><namePart type="family">Seidl</namePart><affiliation>FB IV – Informatik, Universität Trier, D-54286 Trier, Germany</affiliation><affiliation>Corresponding author. Tel.: +49-651-201-2835; fax: +49-651-201-3822</affiliation><affiliation>E-mail: seidl@psi.uni-trier.de</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Christian</namePart><namePart type="family">Fecht</namePart><affiliation>Universität des Saarlandes, Postfach 151150, D-66041 Saarbrücken, Germany</affiliation><role><roleTerm type="text">author</roleTerm></role></name><typeOfResource>text</typeOfResource><genre type="research-article" displayLabel="Full-length article"></genre><originInfo><publisher>ELSEVIER</publisher><dateIssued encoding="w3cdtf">2000</dateIssued><dateModified encoding="w3cdtf">1999-04-30</dateModified><copyrightDate encoding="w3cdtf">2000</copyrightDate></originInfo><language><languageTerm type="code" authority="iso639-2b">eng</languageTerm><languageTerm type="code" authority="rfc3066">en</languageTerm></language><physicalDescription><internetMediaType>text/html</internetMediaType></physicalDescription><abstract 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.</abstract><subject><genre>Keywords</genre><topic>Interprocedural analysis</topic><topic>Pushdown automata</topic><topic>OLDT-resolution</topic><topic>Coincidence theorems</topic></subject><relatedItem type="host"><titleInfo><title>The Journal of Logic Programming</title></titleInfo><titleInfo type="abbreviated"><title>JLP</title></titleInfo><genre type="journal">journal</genre><originInfo><dateIssued encoding="w3cdtf">200005</dateIssued></originInfo><identifier type="ISSN">0743-1066</identifier><identifier type="PII">S0743-1066(00)X0051-9</identifier><part><date>200005</date><detail type="volume"><number>43</number><caption>vol.</caption></detail><detail type="issue"><number>2</number><caption>no.</caption></detail><extent unit="issue pages"><start>123</start><end>186</end></extent><extent unit="pages"><start>123</start><end>156</end></extent></part></relatedItem><identifier type="istex">9BEE7C26B5A58B6EB1657DE6FE82128ADA3F9802</identifier><identifier type="DOI">10.1016/S0743-1066(99)00058-8</identifier><identifier type="PII">S0743-1066(99)00058-8</identifier><accessCondition type="use and reproduction" contentType="copyright">©2000 Elsevier Science Inc.</accessCondition><recordInfo><recordContentSource>ELSEVIER</recordContentSource><recordOrigin>Elsevier Science Inc., ©2000</recordOrigin></recordInfo></mods></metadata><serie></serie></istex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Rhénanie/explor/UnivTrevesV1/Data/Istex/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001663 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 001663 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Rhénanie
|area= UnivTrevesV1
|flux= Istex
|étape= Corpus
|type= RBID
|clé= ISTEX:9BEE7C26B5A58B6EB1657DE6FE82128ADA3F9802
|texte= Interprocedural analyses: a comparison
}}
| This area was generated with Dilib version V0.6.31. |  |