Polynomial constants are decidable
Identifieur interne :
000C40 ( PascalFrancis/Corpus );
précédent :
000C39;
suivant :
000C41
Polynomial constants are decidable
Auteurs : Markus Müller-Olm ;
Helmut SeidlSource :
-
Lecture notes in computer science [ 0302-9743 ] ; 2002.
RBID : Pascal:03-0334456
Descripteurs français
English descriptors
Abstract
Constant propagation aims at identifying expressions that always yield a unique constant value at run-time. It is well-known that constant propagation is undecidable for programs working on integers even if guards are ignored as in non-deterministic flow graphs. We show that polynomial constants are decidable in non-deterministic flow graphs. In polynomial constant propagation, assignment statements that use the operators +, -,* are interpreted exactly but all assignments that use other operators are conservatively interpreted as non-deterministic assignments. We present a generic algorithm for constant propagation via a symbolic weakest precondition computation and show how this generic algorithm can be instantiated for polynomial constant propagation by exploiting techniques from computable ring theory.
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 2477 |
|---|
| A08 | 01 | 1 | ENG | @1 Polynomial constants are decidable |
|---|
| A09 | 01 | 1 | ENG | @1 SAS 2002 : static analysis : Madrid, 17-20 September 2002 |
|---|
| A11 | 01 | 1 | | @1 MÜLLER-OLM (Markus) |
|---|
| A11 | 02 | 1 | | @1 SEIDL (Helmut) |
|---|
| A12 | 01 | 1 | | @1 HERMENEGILDO (Manuel V.) @9 ed. |
|---|
| A12 | 02 | 1 | | @1 PUEBLA (German) @9 ed. |
|---|
| A14 | 01 | | | @1 University of Dortmund, FB 4, LS5 @2 44221 Dortmund @3 DEU @Z 1 aut. |
|---|
| A14 | 02 | | | @1 Trier University, FB 4-Informatik @2 54286 Trier @3 DEU @Z 2 aut. |
|---|
| A20 | | | | @1 4-19 |
|---|
| A21 | | | | @1 2002 |
|---|
| A23 | 01 | | | @0 ENG |
|---|
| A26 | 01 | | | @0 3-540-44235-9 |
|---|
| A43 | 01 | | | @1 INIST @2 16343 @5 354000108467320010 |
|---|
| A44 | | | | @0 0000 @1 © 2003 INIST-CNRS. All rights reserved. |
|---|
| A45 | | | | @0 20 ref. |
|---|
| A47 | 01 | 1 | | @0 03-0334456 |
|---|
| 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 Constant propagation aims at identifying expressions that always yield a unique constant value at run-time. It is well-known that constant propagation is undecidable for programs working on integers even if guards are ignored as in non-deterministic flow graphs. We show that polynomial constants are decidable in non-deterministic flow graphs. In polynomial constant propagation, assignment statements that use the operators +, -,* are interpreted exactly but all assignments that use other operators are conservatively interpreted as non-deterministic assignments. We present a generic algorithm for constant propagation via a symbolic weakest precondition computation and show how this generic algorithm can be instantiated for polynomial constant propagation by exploiting techniques from computable ring theory. |
|---|
| C02 | 01 | X | | @0 001D02A02 |
|---|
| C03 | 01 | X | FRE | @0 Flot graphe @5 01 |
|---|
| C03 | 01 | X | ENG | @0 Graph flow @5 01 |
|---|
| C03 | 01 | X | SPA | @0 Flujo grafo @5 01 |
|---|
| C03 | 02 | X | FRE | @0 Décidabilité @5 02 |
|---|
| C03 | 02 | X | ENG | @0 Decidability @5 02 |
|---|
| C03 | 02 | X | SPA | @0 Decidibilidad @5 02 |
|---|
| C03 | 03 | X | FRE | @0 Non déterminisme @5 03 |
|---|
| C03 | 03 | X | ENG | @0 Non determinism @5 03 |
|---|
| C03 | 03 | X | SPA | @0 No determinismo @5 03 |
|---|
| C03 | 04 | X | FRE | @0 Système non déterministe @5 04 |
|---|
| C03 | 04 | X | ENG | @0 Non deterministic system @5 04 |
|---|
| C03 | 04 | X | SPA | @0 Sistema no determinista @5 04 |
|---|
| C03 | 05 | X | FRE | @0 Flot donnée @5 05 |
|---|
| C03 | 05 | X | ENG | @0 Data flow @5 05 |
|---|
| C03 | 05 | X | SPA | @0 Flujo datos @5 05 |
|---|
| C03 | 06 | 3 | FRE | @0 Graphe flux @5 06 |
|---|
| C03 | 06 | 3 | ENG | @0 Flow graphs @5 06 |
|---|
| C03 | 07 | X | FRE | @0 Graphe fluence @5 07 |
|---|
| C03 | 07 | X | ENG | @0 Fluence graph @5 07 |
|---|
| C03 | 07 | X | SPA | @0 Grafo fluencia @5 07 |
|---|
| C03 | 08 | X | FRE | @0 Constante polynomiale @4 INC @5 82 |
|---|
| N21 | | | | @1 230 |
|---|
| N82 | | | | @1 PSI |
|---|
|
|---|
| pR |
| A30 | 01 | 1 | ENG | @1 International symposium on static analysis @3 Madrid ESP @4 2002-09-17 |
|---|
|
|---|
Format Inist (serveur)
| NO : | PASCAL 03-0334456 INIST |
|---|
| ET : | Polynomial constants are decidable |
|---|
| AU : | MÜLLER-OLM (Markus); SEIDL (Helmut); HERMENEGILDO (Manuel V.); PUEBLA (German) |
|---|
| AF : | University of Dortmund, FB 4, LS5/44221 Dortmund/Allemagne (1 aut.); Trier University, FB 4-Informatik/54286 Trier/Allemagne (2 aut.) |
|---|
| DT : | Publication en série; Congrès; Niveau analytique |
|---|
| SO : | Lecture notes in computer science; ISSN 0302-9743; Allemagne; Da. 2002; Vol. 2477; Pp. 4-19; Bibl. 20 ref. |
|---|
| LA : | Anglais |
|---|
| EA : | Constant propagation aims at identifying expressions that always yield a unique constant value at run-time. It is well-known that constant propagation is undecidable for programs working on integers even if guards are ignored as in non-deterministic flow graphs. We show that polynomial constants are decidable in non-deterministic flow graphs. In polynomial constant propagation, assignment statements that use the operators +, -,* are interpreted exactly but all assignments that use other operators are conservatively interpreted as non-deterministic assignments. We present a generic algorithm for constant propagation via a symbolic weakest precondition computation and show how this generic algorithm can be instantiated for polynomial constant propagation by exploiting techniques from computable ring theory. |
|---|
| CC : | 001D02A02 |
|---|
| FD : | Flot graphe; Décidabilité; Non déterminisme; Système non déterministe; Flot donnée; Graphe flux; Graphe fluence; Constante polynomiale |
|---|
| ED : | Graph flow; Decidability; Non determinism; Non deterministic system; Data flow; Flow graphs; Fluence graph |
|---|
| SD : | Flujo grafo; Decidibilidad; No determinismo; Sistema no determinista; Flujo datos; Grafo fluencia |
|---|
| LO : | INIST-16343.354000108467320010 |
|---|
| ID : | 03-0334456 |
|---|
Links to Exploration step
Pascal:03-0334456
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Polynomial constants are decidable</title>
<author><name sortKey="Muller Olm, Markus" sort="Muller Olm, Markus" uniqKey="Muller Olm M" first="Markus" last="Müller-Olm">Markus Müller-Olm</name>
<affiliation><inist:fA14 i1="01"><s1>University of Dortmund, FB 4, LS5</s1>
<s2>44221 Dortmund</s2>
<s3>DEU</s3>
<sZ>1 aut.</sZ>
</inist:fA14><author><name sortKey="Seidl, Helmut" sort="Seidl, Helmut" uniqKey="Seidl H" first="Helmut" last="Seidl">Helmut Seidl</name>
<affiliation><inist:fA14 i1="02"><s1>Trier University, FB 4-Informatik</s1>
<s2>54286 Trier</s2>
<s3>DEU</s3>
<sZ>2 aut.</sZ>
</inist:fA14><publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">03-0334456</idno>
<date when="2002">2002</date>
<idno type="stanalyst">PASCAL 03-0334456 INIST</idno>
<idno type="RBID">Pascal:03-0334456</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000C40</idno>
</publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Polynomial constants are decidable</title>
<author><name sortKey="Muller Olm, Markus" sort="Muller Olm, Markus" uniqKey="Muller Olm M" first="Markus" last="Müller-Olm">Markus Müller-Olm</name>
<affiliation><inist:fA14 i1="01"><s1>University of Dortmund, FB 4, LS5</s1>
<s2>44221 Dortmund</s2>
<s3>DEU</s3>
<sZ>1 aut.</sZ>
</inist:fA14><author><name sortKey="Seidl, Helmut" sort="Seidl, Helmut" uniqKey="Seidl H" first="Helmut" last="Seidl">Helmut Seidl</name>
<affiliation><inist:fA14 i1="02"><s1>Trier University, FB 4-Informatik</s1>
<s2>54286 Trier</s2>
<s3>DEU</s3>
<sZ>2 aut.</sZ>
</inist:fA14><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><seriesStmt><title level="j" type="main">Lecture notes in computer science</title>
<idno type="ISSN">0302-9743</idno>
</seriesStmt><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Data flow</term>
<term>Decidability</term>
<term>Flow graphs</term>
<term>Fluence graph</term>
<term>Graph flow</term>
<term>Non determinism</term>
<term>Non deterministic system</term>
</keywords><keywords scheme="Pascal" xml:lang="fr"><term>Flot graphe</term>
<term>Décidabilité</term>
<term>Non déterminisme</term>
<term>Système non déterministe</term>
<term>Flot donnée</term>
<term>Graphe flux</term>
<term>Graphe fluence</term>
<term>Constante polynomiale</term>
</keywords><front><div type="abstract" xml:lang="en">Constant propagation aims at identifying expressions that always yield a unique constant value at run-time. It is well-known that constant propagation is undecidable for programs working on integers even if guards are ignored as in non-deterministic flow graphs. We show that polynomial constants are decidable in non-deterministic flow graphs. In polynomial constant propagation, assignment statements that use the operators +, -,* are interpreted exactly but all assignments that use other operators are conservatively interpreted as non-deterministic assignments. We present a generic algorithm for constant propagation via a symbolic weakest precondition computation and show how this generic algorithm can be instantiated for polynomial constant propagation by exploiting techniques from computable ring theory.</div>
</front><inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0302-9743</s0>
</fA01><fA05><s2>2477</s2>
</fA05><fA08 i1="01" i2="1" l="ENG"><s1>Polynomial constants are decidable</s1>
</fA08><fA09 i1="01" i2="1" l="ENG"><s1>SAS 2002 : static analysis : Madrid, 17-20 September 2002</s1>
</fA09><fA11 i1="01" i2="1"><s1>MÜLLER-OLM (Markus)</s1>
</fA11><fA11 i1="02" i2="1"><s1>SEIDL (Helmut)</s1>
</fA11><fA12 i1="01" i2="1"><s1>HERMENEGILDO (Manuel V.)</s1>
<s9>ed.</s9>
</fA12><fA12 i1="02" i2="1"><s1>PUEBLA (German)</s1>
<s9>ed.</s9>
</fA12><fA14 i1="01"><s1>University of Dortmund, FB 4, LS5</s1>
<s2>44221 Dortmund</s2>
<s3>DEU</s3>
<sZ>1 aut.</sZ>
</fA14><fA14 i1="02"><s1>Trier University, FB 4-Informatik</s1>
<s2>54286 Trier</s2>
<s3>DEU</s3>
<sZ>2 aut.</sZ>
</fA14><fA20><s1>4-19</s1>
</fA20><fA21><s1>2002</s1>
</fA21><fA23 i1="01"><s0>ENG</s0>
</fA23><fA26 i1="01"><s0>3-540-44235-9</s0>
</fA26><fA43 i1="01"><s1>INIST</s1>
<s2>16343</s2>
<s5>354000108467320010</s5>
</fA43><fA44><s0>0000</s0>
<s1>© 2003 INIST-CNRS. All rights reserved.</s1>
</fA44><fA45><s0>20 ref.</s0>
</fA45><fA47 i1="01" i2="1"><s0>03-0334456</s0>
</fA47><fA60><s1>P</s1>
<s2>C</s2>
</fA60><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>Constant propagation aims at identifying expressions that always yield a unique constant value at run-time. It is well-known that constant propagation is undecidable for programs working on integers even if guards are ignored as in non-deterministic flow graphs. We show that polynomial constants are decidable in non-deterministic flow graphs. In polynomial constant propagation, assignment statements that use the operators +, -,* are interpreted exactly but all assignments that use other operators are conservatively interpreted as non-deterministic assignments. We present a generic algorithm for constant propagation via a symbolic weakest precondition computation and show how this generic algorithm can be instantiated for polynomial constant propagation by exploiting techniques from computable ring theory.</s0>
</fC01><fC02 i1="01" i2="X"><s0>001D02A02</s0>
</fC02><fC03 i1="01" i2="X" l="FRE"><s0>Flot graphe</s0>
<s5>01</s5>
</fC03><fC03 i1="01" i2="X" l="ENG"><s0>Graph flow</s0>
<s5>01</s5>
</fC03><fC03 i1="01" i2="X" l="SPA"><s0>Flujo grafo</s0>
<s5>01</s5>
</fC03><fC03 i1="02" i2="X" l="FRE"><s0>Décidabilité</s0>
<s5>02</s5>
</fC03><fC03 i1="02" i2="X" l="ENG"><s0>Decidability</s0>
<s5>02</s5>
</fC03><fC03 i1="02" i2="X" l="SPA"><s0>Decidibilidad</s0>
<s5>02</s5>
</fC03><fC03 i1="03" i2="X" l="FRE"><s0>Non déterminisme</s0>
<s5>03</s5>
</fC03><fC03 i1="03" i2="X" l="ENG"><s0>Non determinism</s0>
<s5>03</s5>
</fC03><fC03 i1="03" i2="X" l="SPA"><s0>No determinismo</s0>
<s5>03</s5>
</fC03><fC03 i1="04" i2="X" l="FRE"><s0>Système non déterministe</s0>
<s5>04</s5>
</fC03><fC03 i1="04" i2="X" l="ENG"><s0>Non deterministic system</s0>
<s5>04</s5>
</fC03><fC03 i1="04" i2="X" l="SPA"><s0>Sistema no determinista</s0>
<s5>04</s5>
</fC03><fC03 i1="05" i2="X" l="FRE"><s0>Flot donnée</s0>
<s5>05</s5>
</fC03><fC03 i1="05" i2="X" l="ENG"><s0>Data flow</s0>
<s5>05</s5>
</fC03><fC03 i1="05" i2="X" l="SPA"><s0>Flujo datos</s0>
<s5>05</s5>
</fC03><fC03 i1="06" i2="3" l="FRE"><s0>Graphe flux</s0>
<s5>06</s5>
</fC03><fC03 i1="06" i2="3" l="ENG"><s0>Flow graphs</s0>
<s5>06</s5>
</fC03><fC03 i1="07" i2="X" l="FRE"><s0>Graphe fluence</s0>
<s5>07</s5>
</fC03><fC03 i1="07" i2="X" l="ENG"><s0>Fluence graph</s0>
<s5>07</s5>
</fC03><fC03 i1="07" i2="X" l="SPA"><s0>Grafo fluencia</s0>
<s5>07</s5>
</fC03><fC03 i1="08" i2="X" l="FRE"><s0>Constante polynomiale</s0>
<s4>INC</s4>
<s5>82</s5>
</fC03><fN21><s1>230</s1>
</fN21><fN82><s1>PSI</s1>
</fN82><pR><fA30 i1="01" i2="1" l="ENG"><s1>International symposium on static analysis</s1>
<s3>Madrid ESP</s3>
<s4>2002-09-17</s4>
</fA30><server><NO>PASCAL 03-0334456 INIST</NO>
<ET>Polynomial constants are decidable</ET>
<AU>MÜLLER-OLM (Markus); SEIDL (Helmut); HERMENEGILDO (Manuel V.); PUEBLA (German)</AU>
<AF>University of Dortmund, FB 4, LS5/44221 Dortmund/Allemagne (1 aut.); Trier University, FB 4-Informatik/54286 Trier/Allemagne (2 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. 2477; Pp. 4-19; Bibl. 20 ref.</SO>
<LA>Anglais</LA>
<EA>Constant propagation aims at identifying expressions that always yield a unique constant value at run-time. It is well-known that constant propagation is undecidable for programs working on integers even if guards are ignored as in non-deterministic flow graphs. We show that polynomial constants are decidable in non-deterministic flow graphs. In polynomial constant propagation, assignment statements that use the operators +, -,* are interpreted exactly but all assignments that use other operators are conservatively interpreted as non-deterministic assignments. We present a generic algorithm for constant propagation via a symbolic weakest precondition computation and show how this generic algorithm can be instantiated for polynomial constant propagation by exploiting techniques from computable ring theory.</EA>
<CC>001D02A02</CC>
<FD>Flot graphe; Décidabilité; Non déterminisme; Système non déterministe; Flot donnée; Graphe flux; Graphe fluence; Constante polynomiale</FD>
<ED>Graph flow; Decidability; Non determinism; Non deterministic system; Data flow; Flow graphs; Fluence graph</ED>
<SD>Flujo grafo; Decidibilidad; No determinismo; Sistema no determinista; Flujo datos; Grafo fluencia</SD>
<LO>INIST-16343.354000108467320010</LO>
<ID>03-0334456</ID>
</server>
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 000C40 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Corpus/biblio.hfd -nk 000C40 | 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:03-0334456
|texte= Polynomial constants are decidable
}}
| 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 |  |
