Serveur d'exploration sur l'Université de Trèves

Attention, ce site est en cours de développement !
Attention, site généré par des moyens informatiques à partir de corpus bruts.
Les informations ne sont donc pas validées.

Automatic complexity analysis

Identifieur interne : 000D48 ( PascalFrancis/Corpus ); précédent : 000D47; suivant : 000D49

Automatic complexity analysis

Auteurs : Flemming Nielson ; Hanne Riis Nielson ; Helmut Seidl

Source :

RBID : Pascal:02-0318071

Descripteurs français

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.

Notice en format standard (ISO 2709)

Pour connaître la documentation sur le format Inist Standard.

pA  
A01 01  1    @0 0302-9743
A05       @2 2305
A08 01  1  ENG  @1 Automatic complexity analysis
A09 01  1  ENG  @1 Programming languages and systems : Grenoble, 8-12 April 2002
A11 01  1    @1 NIELSON (Flemming)
A11 02  1    @1 NIELSON (Hanne Riis)
A11 03  1    @1 SEIDL (Helmut)
A12 01  1    @1 LE METAYER (Daniel) @9 ed.
A14 01      @1 Informatics and Mathematical Modelling, The Technical University of Denmark @2 2800 Kongens Lyngby @3 DNK @Z 1 aut. @Z 2 aut.
A14 02      @1 Fachbereich IV - Informatik, Universität Trier @2 54286 Trier @3 DEU @Z 3 aut.
A20       @1 243-261
A21       @1 2002
A23 01      @0 ENG
A26 01      @0 3-540-43363-5
A43 01      @1 INIST @2 16343 @5 354000097089760180
A44       @0 0000 @1 © 2002 INIST-CNRS. All rights reserved.
A45       @0 14 ref.
A47 01  1    @0 02-0318071
A60       @1 P @2 C
A61       @0 A
A64 01  1    @0 Lecture notes in computer science
A66 01      @0 DEU
C01 01    ENG  @0 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.
C02 01  X    @0 001D02A02
C03 01  3  FRE  @0 Clause Horn @5 01
C03 01  3  ENG  @0 Horn clauses @5 01
C03 02  X  FRE  @0 Comportement asymptotique @5 02
C03 02  X  ENG  @0 Asymptotic behavior @5 02
C03 02  X  SPA  @0 Comportamiento asintótico @5 02
C03 03  X  FRE  @0 Analyse automatique @5 03
C03 03  X  ENG  @0 Automatic analysis @5 03
C03 03  X  SPA  @0 Análisis automático @5 03
C03 04  X  FRE  @0 Analyse programme @5 04
C03 04  X  ENG  @0 Program analysis @5 04
C03 04  X  SPA  @0 Análisis programa @5 04
C03 05  X  FRE  @0 Matrice creuse @5 05
C03 05  X  ENG  @0 Sparse matrix @5 05
C03 05  X  SPA  @0 Matriz dispersa @5 05
N21       @1 175
N82       @1 PSI
pR  
A30 01  1  ENG  @1 ESOP 2002 : European symposium on programming @2 11 @3 Grenoble FRA @4 2002-04-08

Format Inist (serveur)

NO : PASCAL 02-0318071 INIST
ET : Automatic complexity analysis
AU : NIELSON (Flemming); NIELSON (Hanne Riis); SEIDL (Helmut); LE METAYER (Daniel)
AF : Informatics and Mathematical Modelling, The Technical University of Denmark/2800 Kongens Lyngby/Danemark (1 aut., 2 aut.); Fachbereich IV - Informatik, Universität Trier/54286 Trier/Allemagne (3 aut.)
DT : Publication en série; Congrès; Niveau analytique
SO : Lecture notes in computer science; ISSN 0302-9743; Allemagne; Da. 2002; Vol. 2305; Pp. 243-261; Bibl. 14 ref.
LA : Anglais
EA : 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.
CC : 001D02A02
FD : Clause Horn; Comportement asymptotique; Analyse automatique; Analyse programme; Matrice creuse
ED : Horn clauses; Asymptotic behavior; Automatic analysis; Program analysis; Sparse matrix
SD : Comportamiento asintótico; Análisis automático; Análisis programa; Matriz dispersa
LO : INIST-16343.354000097089760180
ID : 02-0318071

Links to Exploration step

Pascal:02-0318071

Le 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>
<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>
</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>
<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>
</affiliation>
</author>
<author>
<name sortKey="Seidl, Helmut" sort="Seidl, Helmut" uniqKey="Seidl H" first="Helmut" last="Seidl">Helmut Seidl</name>
<affiliation>
<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>
</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>
</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>
<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>
</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>
<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>
</affiliation>
</author>
<author>
<name sortKey="Seidl, Helmut" sort="Seidl, Helmut" uniqKey="Seidl H" first="Helmut" last="Seidl">Helmut Seidl</name>
<affiliation>
<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>
</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>
<server>
<NO>PASCAL 02-0318071 INIST</NO>
<ET>Automatic complexity analysis</ET>
<AU>NIELSON (Flemming); NIELSON (Hanne Riis); SEIDL (Helmut); LE METAYER (Daniel)</AU>
<AF>Informatics and Mathematical Modelling, The Technical University of Denmark/2800 Kongens Lyngby/Danemark (1 aut., 2 aut.); Fachbereich IV - Informatik, Universität Trier/54286 Trier/Allemagne (3 aut.)</AF>
<DT>Publication en série; Congrès; Niveau analytique</DT>
<SO>Lecture notes in computer science; ISSN 0302-9743; Allemagne; Da. 2002; Vol. 2305; Pp. 243-261; Bibl. 14 ref.</SO>
<LA>Anglais</LA>
<EA>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.</EA>
<CC>001D02A02</CC>
<FD>Clause Horn; Comportement asymptotique; Analyse automatique; Analyse programme; Matrice creuse</FD>
<ED>Horn clauses; Asymptotic behavior; Automatic analysis; Program analysis; Sparse matrix</ED>
<SD>Comportamiento asintótico; Análisis automático; Análisis programa; Matriz dispersa</SD>
<LO>INIST-16343.354000097089760180</LO>
<ID>02-0318071</ID>
</server>
</inist>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Rhénanie/explor/UnivTrevesV1/Data/PascalFrancis/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000D48 | SxmlIndent | more

Ou

HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Corpus/biblio.hfd -nk 000D48 | 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=   Corpus
   |type=    RBID
   |clé=     Pascal:02-0318071
   |texte=   Automatic complexity analysis
}}

Wicri

This area was generated with Dilib version V0.6.31.
Data generation: Sat Jul 22 16:29:01 2017. Site generation: Wed Feb 28 14:55:37 2024