Automatic complexity analysis
Identifieur interne : 000B22 ( PascalFrancis/Checkpoint ); précédent : 000B21; suivant : 000B23Automatic complexity analysis
Auteurs : Flemming Nielson [Danemark] ; Hanne Riis Nielson [Danemark] ; Helmut Seidl [Allemagne]Source :
- Lecture notes in computer science [ 0302-9743 ] ; 2002.
Descripteurs français
- Pascal (Inist)
English descriptors
Abstract
We consider the problem of automating the derivation of tight asymptotic complexity bounds for solving Horn clauses. Clearly, the solving time crucially depends on the "sparseness" of the computed relations. Therefore, our asymptotic runtime analysis is accompanied by an asymptotic sparsity calculus together with an asymptotic sparsity analysis. The technical problem here is that least fixpoint iteration fails on asymptotic complexity expressions: the intuitive reason is that O(1)+ O(1) = O(1) but O(1) +...+ O(1) may return any value.
Affiliations:
Links toward previous steps (curation, corpus...)
Links to Exploration step
Pascal:02-0318071Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Automatic complexity analysis</title><author><name sortKey="Nielson, Flemming" sort="Nielson, Flemming" uniqKey="Nielson F" first="Flemming" last="Nielson">Flemming Nielson</name><affiliation wicri:level="1"><inist:fA14 i1="01"><s1>Informatics and Mathematical Modelling, The Technical University of Denmark</s1><s2>2800 Kongens Lyngby</s2><s3>DNK</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ></inist:fA14><country>Danemark</country><wicri:noRegion>2800 Kongens Lyngby</wicri:noRegion></affiliation></author><author><name sortKey="Nielson, Hanne Riis" sort="Nielson, Hanne Riis" uniqKey="Nielson H" first="Hanne Riis" last="Nielson">Hanne Riis Nielson</name><affiliation wicri:level="1"><inist:fA14 i1="01"><s1>Informatics and Mathematical Modelling, The Technical University of Denmark</s1><s2>2800 Kongens Lyngby</s2><s3>DNK</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ></inist:fA14><country>Danemark</country><wicri:noRegion>2800 Kongens Lyngby</wicri:noRegion></affiliation></author><author><name sortKey="Seidl, Helmut" sort="Seidl, Helmut" uniqKey="Seidl H" first="Helmut" last="Seidl">Helmut Seidl</name><affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Fachbereich IV - Informatik, Universität Trier</s1><s2>54286 Trier</s2><s3>DEU</s3><sZ>3 aut.</sZ></inist:fA14><country>Allemagne</country><wicri:noRegion>54286 Trier</wicri:noRegion><wicri:noRegion>Universität Trier</wicri:noRegion><wicri:noRegion>54286 Trier</wicri:noRegion></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">INIST</idno><idno type="inist">02-0318071</idno><date when="2002">2002</date><idno type="stanalyst">PASCAL 02-0318071 INIST</idno><idno type="RBID">Pascal:02-0318071</idno><idno type="wicri:Area/PascalFrancis/Corpus">000D48</idno><idno type="wicri:Area/PascalFrancis/Curation">000188</idno><idno type="wicri:Area/PascalFrancis/Checkpoint">000B22</idno><idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000B22</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Automatic complexity analysis</title><author><name sortKey="Nielson, Flemming" sort="Nielson, Flemming" uniqKey="Nielson F" first="Flemming" last="Nielson">Flemming Nielson</name><affiliation wicri:level="1"><inist:fA14 i1="01"><s1>Informatics and Mathematical Modelling, The Technical University of Denmark</s1><s2>2800 Kongens Lyngby</s2><s3>DNK</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ></inist:fA14><country>Danemark</country><wicri:noRegion>2800 Kongens Lyngby</wicri:noRegion></affiliation></author><author><name sortKey="Nielson, Hanne Riis" sort="Nielson, Hanne Riis" uniqKey="Nielson H" first="Hanne Riis" last="Nielson">Hanne Riis Nielson</name><affiliation wicri:level="1"><inist:fA14 i1="01"><s1>Informatics and Mathematical Modelling, The Technical University of Denmark</s1><s2>2800 Kongens Lyngby</s2><s3>DNK</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ></inist:fA14><country>Danemark</country><wicri:noRegion>2800 Kongens Lyngby</wicri:noRegion></affiliation></author><author><name sortKey="Seidl, Helmut" sort="Seidl, Helmut" uniqKey="Seidl H" first="Helmut" last="Seidl">Helmut Seidl</name><affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Fachbereich IV - Informatik, Universität Trier</s1><s2>54286 Trier</s2><s3>DEU</s3><sZ>3 aut.</sZ></inist:fA14><country>Allemagne</country><wicri:noRegion>54286 Trier</wicri:noRegion><wicri:noRegion>Universität Trier</wicri:noRegion><wicri:noRegion>54286 Trier</wicri:noRegion></affiliation></author></analytic><series><title level="j" type="main">Lecture notes in computer science</title><idno type="ISSN">0302-9743</idno><imprint><date when="2002">2002</date></imprint></series></biblStruct></sourceDesc><seriesStmt><title level="j" type="main">Lecture notes in computer science</title><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Asymptotic behavior</term><term>Automatic analysis</term><term>Horn clauses</term><term>Program analysis</term><term>Sparse matrix</term></keywords><keywords scheme="Pascal" xml:lang="fr"><term>Clause Horn</term><term>Comportement asymptotique</term><term>Analyse automatique</term><term>Analyse programme</term><term>Matrice creuse</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">We consider the problem of automating the derivation of tight asymptotic complexity bounds for solving Horn clauses. Clearly, the solving time crucially depends on the "sparseness" of the computed relations. Therefore, our asymptotic runtime analysis is accompanied by an asymptotic sparsity calculus together with an asymptotic sparsity analysis. The technical problem here is that least fixpoint iteration fails on asymptotic complexity expressions: the intuitive reason is that O(1)+ O(1) = O(1) but O(1) +...+ O(1) may return any value.</div></front></TEI><inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0302-9743</s0></fA01><fA05><s2>2305</s2></fA05><fA08 i1="01" i2="1" l="ENG"><s1>Automatic complexity analysis</s1></fA08><fA09 i1="01" i2="1" l="ENG"><s1>Programming languages and systems : Grenoble, 8-12 April 2002</s1></fA09><fA11 i1="01" i2="1"><s1>NIELSON (Flemming)</s1></fA11><fA11 i1="02" i2="1"><s1>NIELSON (Hanne Riis)</s1></fA11><fA11 i1="03" i2="1"><s1>SEIDL (Helmut)</s1></fA11><fA12 i1="01" i2="1"><s1>LE METAYER (Daniel)</s1><s9>ed.</s9></fA12><fA14 i1="01"><s1>Informatics and Mathematical Modelling, The Technical University of Denmark</s1><s2>2800 Kongens Lyngby</s2><s3>DNK</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ></fA14><fA14 i1="02"><s1>Fachbereich IV - Informatik, Universität Trier</s1><s2>54286 Trier</s2><s3>DEU</s3><sZ>3 aut.</sZ></fA14><fA20><s1>243-261</s1></fA20><fA21><s1>2002</s1></fA21><fA23 i1="01"><s0>ENG</s0></fA23><fA26 i1="01"><s0>3-540-43363-5</s0></fA26><fA43 i1="01"><s1>INIST</s1><s2>16343</s2><s5>354000097089760180</s5></fA43><fA44><s0>0000</s0><s1>© 2002 INIST-CNRS. All rights reserved.</s1></fA44><fA45><s0>14 ref.</s0></fA45><fA47 i1="01" i2="1"><s0>02-0318071</s0></fA47><fA60><s1>P</s1><s2>C</s2></fA60><fA61><s0>A</s0></fA61><fA64 i1="01" i2="1"><s0>Lecture notes in computer science</s0></fA64><fA66 i1="01"><s0>DEU</s0></fA66><fC01 i1="01" l="ENG"><s0>We consider the problem of automating the derivation of tight asymptotic complexity bounds for solving Horn clauses. Clearly, the solving time crucially depends on the "sparseness" of the computed relations. Therefore, our asymptotic runtime analysis is accompanied by an asymptotic sparsity calculus together with an asymptotic sparsity analysis. The technical problem here is that least fixpoint iteration fails on asymptotic complexity expressions: the intuitive reason is that O(1)+ O(1) = O(1) but O(1) +...+ O(1) may return any value.</s0></fC01><fC02 i1="01" i2="X"><s0>001D02A02</s0></fC02><fC03 i1="01" i2="3" l="FRE"><s0>Clause Horn</s0><s5>01</s5></fC03><fC03 i1="01" i2="3" l="ENG"><s0>Horn clauses</s0><s5>01</s5></fC03><fC03 i1="02" i2="X" l="FRE"><s0>Comportement asymptotique</s0><s5>02</s5></fC03><fC03 i1="02" i2="X" l="ENG"><s0>Asymptotic behavior</s0><s5>02</s5></fC03><fC03 i1="02" i2="X" l="SPA"><s0>Comportamiento asintótico</s0><s5>02</s5></fC03><fC03 i1="03" i2="X" l="FRE"><s0>Analyse automatique</s0><s5>03</s5></fC03><fC03 i1="03" i2="X" l="ENG"><s0>Automatic analysis</s0><s5>03</s5></fC03><fC03 i1="03" i2="X" l="SPA"><s0>Análisis automático</s0><s5>03</s5></fC03><fC03 i1="04" i2="X" l="FRE"><s0>Analyse programme</s0><s5>04</s5></fC03><fC03 i1="04" i2="X" l="ENG"><s0>Program analysis</s0><s5>04</s5></fC03><fC03 i1="04" i2="X" l="SPA"><s0>Análisis programa</s0><s5>04</s5></fC03><fC03 i1="05" i2="X" l="FRE"><s0>Matrice creuse</s0><s5>05</s5></fC03><fC03 i1="05" i2="X" l="ENG"><s0>Sparse matrix</s0><s5>05</s5></fC03><fC03 i1="05" i2="X" l="SPA"><s0>Matriz dispersa</s0><s5>05</s5></fC03><fN21><s1>175</s1></fN21><fN82><s1>PSI</s1></fN82></pA><pR><fA30 i1="01" i2="1" l="ENG"><s1>ESOP 2002 : European symposium on programming</s1><s2>11</s2><s3>Grenoble FRA</s3><s4>2002-04-08</s4></fA30></pR></standard></inist><affiliations><list><country><li>Allemagne</li><li>Danemark</li></country></list><tree><country name="Danemark"><noRegion><name sortKey="Nielson, Flemming" sort="Nielson, Flemming" uniqKey="Nielson F" first="Flemming" last="Nielson">Flemming Nielson</name></noRegion><name sortKey="Nielson, Hanne Riis" sort="Nielson, Hanne Riis" uniqKey="Nielson H" first="Hanne Riis" last="Nielson">Hanne Riis Nielson</name></country><country name="Allemagne"><noRegion><name sortKey="Seidl, Helmut" sort="Seidl, Helmut" uniqKey="Seidl H" first="Helmut" last="Seidl">Helmut 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 000B22 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Checkpoint/biblio.hfd -nk 000B22 | 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:02-0318071
|texte= Automatic complexity analysis
}}
| This area was generated with Dilib version V0.6.31. |  |