Combining data structures with nonstably infinite theories using many-sorted logic
Identifieur interne :
000509 ( PascalFrancis/Corpus );
précédent :
000508;
suivant :
000510
Combining data structures with nonstably infinite theories using many-sorted logic
Auteurs : Silvio Ranise ;
Christophe Ringeissen ;
Calogero G. ZarbaSource :
-
Lecture notes in computer science [ 0302-9743 ] ; 2005.
RBID : Pascal:05-0449866
Descripteurs français
English descriptors
Abstract
Most computer programs store elements of a given nature into container-based data structures such as lists, arrays, sets, and multisets. To verify the correctness of these programs, one needs to combine a theory S modeling the data structure with a theory T modeling the elements. This combination can be achieved using the classic Nelson-Oppen method only if both S and T are stably infinite. The goal of this paper is to relax the stable infiniteness requirement. To achieve this goal, we introduce the notion of polite theories, and we show that natural examples of polite theories include those modeling data structures such as lists, arrays, sets, and multisets. Furthemore, we provide a method that is able to combine a polite theory S with any theory T of the elements, regardless of whether T is stably infinite or not. The results of this paper generalize to many-sorted logic those recently obtained by Tinelli and Zarba concerning the combination of shiny theories with nonstably infinite theories in one-sorted logic.
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 3717 |
|---|
| A08 | 01 | 1 | ENG | @1 Combining data structures with nonstably infinite theories using many-sorted logic |
|---|
| A09 | 01 | 1 | ENG | @1 Frontiers of combining systems : 5th international workshop, FroCoS 2005, Vienna, Austria, September 19-21, 2005, proceedings |
|---|
| A11 | 01 | 1 | | @1 RANISE (Silvio) |
|---|
| A11 | 02 | 1 | | @1 RINGEISSEN (Christophe) |
|---|
| A11 | 03 | 1 | | @1 ZARBA (Calogero G.) |
|---|
| A14 | 01 | | | @1 LORIA and INRIA-Lorraine @3 USA @Z 1 aut. @Z 2 aut. |
|---|
| A14 | 02 | | | @1 University of New Mexico @3 USA @Z 3 aut. |
|---|
| A20 | | | | @1 48-64 |
|---|
| A21 | | | | @1 2005 |
|---|
| A23 | 01 | | | @0 ENG |
|---|
| A26 | 01 | | | @0 3-540-29051-6 |
|---|
| A43 | 01 | | | @1 INIST @2 16343 @5 354000124514080030 |
|---|
| A44 | | | | @0 0000 @1 © 2005 INIST-CNRS. All rights reserved. |
|---|
| A45 | | | | @0 15 ref. |
|---|
| A47 | 01 | 1 | | @0 05-0449866 |
|---|
| A60 | | | | @1 P @2 C |
|---|
| A61 | | | | @0 A |
|---|
| A64 | 01 | 1 | | @0 Lecture notes in computer science |
|---|
| A66 | 01 | | | @0 USA |
|---|
| C01 | 01 | | ENG | @0 Most computer programs store elements of a given nature into container-based data structures such as lists, arrays, sets, and multisets. To verify the correctness of these programs, one needs to combine a theory S modeling the data structure with a theory T modeling the elements. This combination can be achieved using the classic Nelson-Oppen method only if both S and T are stably infinite. The goal of this paper is to relax the stable infiniteness requirement. To achieve this goal, we introduce the notion of polite theories, and we show that natural examples of polite theories include those modeling data structures such as lists, arrays, sets, and multisets. Furthemore, we provide a method that is able to combine a polite theory S with any theory T of the elements, regardless of whether T is stably infinite or not. The results of this paper generalize to many-sorted logic those recently obtained by Tinelli and Zarba concerning the combination of shiny theories with nonstably infinite theories in one-sorted logic. |
|---|
| C02 | 01 | X | | @0 001D02A04 |
|---|
| C03 | 01 | X | FRE | @0 Programmation logique @5 01 |
|---|
| C03 | 01 | X | ENG | @0 Logical programming @5 01 |
|---|
| C03 | 01 | X | SPA | @0 Programación lógica @5 01 |
|---|
| C03 | 02 | X | FRE | @0 Structure donnée @5 06 |
|---|
| C03 | 02 | X | ENG | @0 Data structure @5 06 |
|---|
| C03 | 02 | X | SPA | @0 Estructura datos @5 06 |
|---|
| C03 | 03 | X | FRE | @0 Conteneur @5 18 |
|---|
| C03 | 03 | X | ENG | @0 Container @5 18 |
|---|
| C03 | 03 | X | SPA | @0 Contenedor @5 18 |
|---|
| C03 | 04 | X | FRE | @0 Exactitude programme @5 19 |
|---|
| C03 | 04 | X | ENG | @0 Program correctness @5 19 |
|---|
| C03 | 04 | X | SPA | @0 Exactitud programa @5 19 |
|---|
| C03 | 05 | X | FRE | @0 Programme ordinateur @5 23 |
|---|
| C03 | 05 | X | ENG | @0 Computer program @5 23 |
|---|
| C03 | 05 | X | SPA | @0 Programa informático @5 23 |
|---|
| C03 | 06 | X | FRE | @0 Multiplicité @5 24 |
|---|
| C03 | 06 | X | ENG | @0 Multiplicity @5 24 |
|---|
| C03 | 06 | X | SPA | @0 Multiplicidad @5 24 |
|---|
| C03 | 07 | X | FRE | @0 Modélisation @5 25 |
|---|
| C03 | 07 | X | ENG | @0 Modeling @5 25 |
|---|
| C03 | 07 | X | SPA | @0 Modelización @5 25 |
|---|
| C03 | 08 | X | FRE | @0 Multiensemble @4 CD @5 96 |
|---|
| C03 | 08 | X | ENG | @0 Multiset @4 CD @5 96 |
|---|
| C03 | 08 | X | SPA | @0 Multiconjunto @4 CD @5 96 |
|---|
| N21 | | | | @1 311 |
|---|
| N44 | 01 | | | @1 OTO |
|---|
| N82 | | | | @1 OTO |
|---|
|
|---|
| pR |
| A30 | 01 | 1 | ENG | @1 FroCoS : frontiers of combining systems. International workshop @2 5 @3 Vienna AUT @4 2005-09-19 |
|---|
|
|---|
Format Inist (serveur)
| NO : | PASCAL 05-0449866 INIST |
|---|
| ET : | Combining data structures with nonstably infinite theories using many-sorted logic |
|---|
| AU : | RANISE (Silvio); RINGEISSEN (Christophe); ZARBA (Calogero G.) |
|---|
| AF : | LORIA and INRIA-Lorraine/Etats-Unis (1 aut., 2 aut.); University of New Mexico/Etats-Unis (3 aut.) |
|---|
| DT : | Publication en série; Congrès; Niveau analytique |
|---|
| SO : | Lecture notes in computer science; ISSN 0302-9743; Etats-Unis; Da. 2005; Vol. 3717; Pp. 48-64; Bibl. 15 ref. |
|---|
| LA : | Anglais |
|---|
| EA : | Most computer programs store elements of a given nature into container-based data structures such as lists, arrays, sets, and multisets. To verify the correctness of these programs, one needs to combine a theory S modeling the data structure with a theory T modeling the elements. This combination can be achieved using the classic Nelson-Oppen method only if both S and T are stably infinite. The goal of this paper is to relax the stable infiniteness requirement. To achieve this goal, we introduce the notion of polite theories, and we show that natural examples of polite theories include those modeling data structures such as lists, arrays, sets, and multisets. Furthemore, we provide a method that is able to combine a polite theory S with any theory T of the elements, regardless of whether T is stably infinite or not. The results of this paper generalize to many-sorted logic those recently obtained by Tinelli and Zarba concerning the combination of shiny theories with nonstably infinite theories in one-sorted logic. |
|---|
| CC : | 001D02A04 |
|---|
| FD : | Programmation logique; Structure donnée; Conteneur; Exactitude programme; Programme ordinateur; Multiplicité; Modélisation; Multiensemble |
|---|
| ED : | Logical programming; Data structure; Container; Program correctness; Computer program; Multiplicity; Modeling; Multiset |
|---|
| SD : | Programación lógica; Estructura datos; Contenedor; Exactitud programa; Programa informático; Multiplicidad; Modelización; Multiconjunto |
|---|
| LO : | INIST-16343.354000124514080030 |
|---|
| ID : | 05-0449866 |
|---|
Links to Exploration step
Pascal:05-0449866
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Combining data structures with nonstably infinite theories using many-sorted logic</title>
<author><name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name>
<affiliation><inist:fA14 i1="01"><s1>LORIA and INRIA-Lorraine</s1>
<s3>USA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14><author><name sortKey="Ringeissen, Christophe" sort="Ringeissen, Christophe" uniqKey="Ringeissen C" first="Christophe" last="Ringeissen">Christophe Ringeissen</name>
<affiliation><inist:fA14 i1="01"><s1>LORIA and INRIA-Lorraine</s1>
<s3>USA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14><author><name sortKey="Zarba, Calogero G" sort="Zarba, Calogero G" uniqKey="Zarba C" first="Calogero G." last="Zarba">Calogero G. Zarba</name>
<affiliation><inist:fA14 i1="02"><s1>University of New Mexico</s1>
<s3>USA</s3>
<sZ>3 aut.</sZ>
</inist:fA14><publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">05-0449866</idno>
<date when="2005">2005</date>
<idno type="stanalyst">PASCAL 05-0449866 INIST</idno>
<idno type="RBID">Pascal:05-0449866</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000509</idno>
</publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Combining data structures with nonstably infinite theories using many-sorted logic</title>
<author><name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name>
<affiliation><inist:fA14 i1="01"><s1>LORIA and INRIA-Lorraine</s1>
<s3>USA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14><author><name sortKey="Ringeissen, Christophe" sort="Ringeissen, Christophe" uniqKey="Ringeissen C" first="Christophe" last="Ringeissen">Christophe Ringeissen</name>
<affiliation><inist:fA14 i1="01"><s1>LORIA and INRIA-Lorraine</s1>
<s3>USA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14><author><name sortKey="Zarba, Calogero G" sort="Zarba, Calogero G" uniqKey="Zarba C" first="Calogero G." last="Zarba">Calogero G. Zarba</name>
<affiliation><inist:fA14 i1="02"><s1>University of New Mexico</s1>
<s3>USA</s3>
<sZ>3 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="2005">2005</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>Computer program</term>
<term>Container</term>
<term>Data structure</term>
<term>Logical programming</term>
<term>Modeling</term>
<term>Multiplicity</term>
<term>Multiset</term>
<term>Program correctness</term>
</keywords><keywords scheme="Pascal" xml:lang="fr"><term>Programmation logique</term>
<term>Structure donnée</term>
<term>Conteneur</term>
<term>Exactitude programme</term>
<term>Programme ordinateur</term>
<term>Multiplicité</term>
<term>Modélisation</term>
<term>Multiensemble</term>
</keywords><front><div type="abstract" xml:lang="en">Most computer programs store elements of a given nature into container-based data structures such as lists, arrays, sets, and multisets. To verify the correctness of these programs, one needs to combine a theory S modeling the data structure with a theory T modeling the elements. This combination can be achieved using the classic Nelson-Oppen method only if both S and T are stably infinite. The goal of this paper is to relax the stable infiniteness requirement. To achieve this goal, we introduce the notion of polite theories, and we show that natural examples of polite theories include those modeling data structures such as lists, arrays, sets, and multisets. Furthemore, we provide a method that is able to combine a polite theory S with any theory T of the elements, regardless of whether T is stably infinite or not. The results of this paper generalize to many-sorted logic those recently obtained by Tinelli and Zarba concerning the combination of shiny theories with nonstably infinite theories in one-sorted logic.</div>
</front><inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0302-9743</s0>
</fA01><fA05><s2>3717</s2>
</fA05><fA08 i1="01" i2="1" l="ENG"><s1>Combining data structures with nonstably infinite theories using many-sorted logic</s1>
</fA08><fA09 i1="01" i2="1" l="ENG"><s1>Frontiers of combining systems : 5th international workshop, FroCoS 2005, Vienna, Austria, September 19-21, 2005, proceedings</s1>
</fA09><fA11 i1="01" i2="1"><s1>RANISE (Silvio)</s1>
</fA11><fA11 i1="02" i2="1"><s1>RINGEISSEN (Christophe)</s1>
</fA11><fA11 i1="03" i2="1"><s1>ZARBA (Calogero G.)</s1>
</fA11><fA14 i1="01"><s1>LORIA and INRIA-Lorraine</s1>
<s3>USA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</fA14><fA14 i1="02"><s1>University of New Mexico</s1>
<s3>USA</s3>
<sZ>3 aut.</sZ>
</fA14><fA20><s1>48-64</s1>
</fA20><fA21><s1>2005</s1>
</fA21><fA23 i1="01"><s0>ENG</s0>
</fA23><fA26 i1="01"><s0>3-540-29051-6</s0>
</fA26><fA43 i1="01"><s1>INIST</s1>
<s2>16343</s2>
<s5>354000124514080030</s5>
</fA43><fA44><s0>0000</s0>
<s1>© 2005 INIST-CNRS. All rights reserved.</s1>
</fA44><fA45><s0>15 ref.</s0>
</fA45><fA47 i1="01" i2="1"><s0>05-0449866</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>USA</s0>
</fA66><fC01 i1="01" l="ENG"><s0>Most computer programs store elements of a given nature into container-based data structures such as lists, arrays, sets, and multisets. To verify the correctness of these programs, one needs to combine a theory S modeling the data structure with a theory T modeling the elements. This combination can be achieved using the classic Nelson-Oppen method only if both S and T are stably infinite. The goal of this paper is to relax the stable infiniteness requirement. To achieve this goal, we introduce the notion of polite theories, and we show that natural examples of polite theories include those modeling data structures such as lists, arrays, sets, and multisets. Furthemore, we provide a method that is able to combine a polite theory S with any theory T of the elements, regardless of whether T is stably infinite or not. The results of this paper generalize to many-sorted logic those recently obtained by Tinelli and Zarba concerning the combination of shiny theories with nonstably infinite theories in one-sorted logic.</s0>
</fC01><fC02 i1="01" i2="X"><s0>001D02A04</s0>
</fC02><fC03 i1="01" i2="X" l="FRE"><s0>Programmation logique</s0>
<s5>01</s5>
</fC03><fC03 i1="01" i2="X" l="ENG"><s0>Logical programming</s0>
<s5>01</s5>
</fC03><fC03 i1="01" i2="X" l="SPA"><s0>Programación lógica</s0>
<s5>01</s5>
</fC03><fC03 i1="02" i2="X" l="FRE"><s0>Structure donnée</s0>
<s5>06</s5>
</fC03><fC03 i1="02" i2="X" l="ENG"><s0>Data structure</s0>
<s5>06</s5>
</fC03><fC03 i1="02" i2="X" l="SPA"><s0>Estructura datos</s0>
<s5>06</s5>
</fC03><fC03 i1="03" i2="X" l="FRE"><s0>Conteneur</s0>
<s5>18</s5>
</fC03><fC03 i1="03" i2="X" l="ENG"><s0>Container</s0>
<s5>18</s5>
</fC03><fC03 i1="03" i2="X" l="SPA"><s0>Contenedor</s0>
<s5>18</s5>
</fC03><fC03 i1="04" i2="X" l="FRE"><s0>Exactitude programme</s0>
<s5>19</s5>
</fC03><fC03 i1="04" i2="X" l="ENG"><s0>Program correctness</s0>
<s5>19</s5>
</fC03><fC03 i1="04" i2="X" l="SPA"><s0>Exactitud programa</s0>
<s5>19</s5>
</fC03><fC03 i1="05" i2="X" l="FRE"><s0>Programme ordinateur</s0>
<s5>23</s5>
</fC03><fC03 i1="05" i2="X" l="ENG"><s0>Computer program</s0>
<s5>23</s5>
</fC03><fC03 i1="05" i2="X" l="SPA"><s0>Programa informático</s0>
<s5>23</s5>
</fC03><fC03 i1="06" i2="X" l="FRE"><s0>Multiplicité</s0>
<s5>24</s5>
</fC03><fC03 i1="06" i2="X" l="ENG"><s0>Multiplicity</s0>
<s5>24</s5>
</fC03><fC03 i1="06" i2="X" l="SPA"><s0>Multiplicidad</s0>
<s5>24</s5>
</fC03><fC03 i1="07" i2="X" l="FRE"><s0>Modélisation</s0>
<s5>25</s5>
</fC03><fC03 i1="07" i2="X" l="ENG"><s0>Modeling</s0>
<s5>25</s5>
</fC03><fC03 i1="07" i2="X" l="SPA"><s0>Modelización</s0>
<s5>25</s5>
</fC03><fC03 i1="08" i2="X" l="FRE"><s0>Multiensemble</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03><fC03 i1="08" i2="X" l="ENG"><s0>Multiset</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03><fC03 i1="08" i2="X" l="SPA"><s0>Multiconjunto</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03><fN21><s1>311</s1>
</fN21><fN44 i1="01"><s1>OTO</s1>
</fN44><fN82><s1>OTO</s1>
</fN82><pR><fA30 i1="01" i2="1" l="ENG"><s1>FroCoS : frontiers of combining systems. International workshop</s1>
<s2>5</s2>
<s3>Vienna AUT</s3>
<s4>2005-09-19</s4>
</fA30><server><NO>PASCAL 05-0449866 INIST</NO>
<ET>Combining data structures with nonstably infinite theories using many-sorted logic</ET>
<AU>RANISE (Silvio); RINGEISSEN (Christophe); ZARBA (Calogero G.)</AU>
<AF>LORIA and INRIA-Lorraine/Etats-Unis (1 aut., 2 aut.); University of New Mexico/Etats-Unis (3 aut.)</AF>
<DT>Publication en série; Congrès; Niveau analytique</DT>
<SO>Lecture notes in computer science; ISSN 0302-9743; Etats-Unis; Da. 2005; Vol. 3717; Pp. 48-64; Bibl. 15 ref.</SO>
<LA>Anglais</LA>
<EA>Most computer programs store elements of a given nature into container-based data structures such as lists, arrays, sets, and multisets. To verify the correctness of these programs, one needs to combine a theory S modeling the data structure with a theory T modeling the elements. This combination can be achieved using the classic Nelson-Oppen method only if both S and T are stably infinite. The goal of this paper is to relax the stable infiniteness requirement. To achieve this goal, we introduce the notion of polite theories, and we show that natural examples of polite theories include those modeling data structures such as lists, arrays, sets, and multisets. Furthemore, we provide a method that is able to combine a polite theory S with any theory T of the elements, regardless of whether T is stably infinite or not. The results of this paper generalize to many-sorted logic those recently obtained by Tinelli and Zarba concerning the combination of shiny theories with nonstably infinite theories in one-sorted logic.</EA>
<CC>001D02A04</CC>
<FD>Programmation logique; Structure donnée; Conteneur; Exactitude programme; Programme ordinateur; Multiplicité; Modélisation; Multiensemble</FD>
<ED>Logical programming; Data structure; Container; Program correctness; Computer program; Multiplicity; Modeling; Multiset</ED>
<SD>Programación lógica; Estructura datos; Contenedor; Exactitud programa; Programa informático; Multiplicidad; Modelización; Multiconjunto</SD>
<LO>INIST-16343.354000124514080030</LO>
<ID>05-0449866</ID>
</server>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/PascalFrancis/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000509 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Corpus/biblio.hfd -nk 000509 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= PascalFrancis
|étape= Corpus
|type= RBID
|clé= Pascal:05-0449866
|texte= Combining data structures with nonstably infinite theories using many-sorted logic
}}
| This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022 |  |
