InforLorV4, Main, Exploration, bibRecord, 006288

Combining Data Structures with Nonstably Infinite Theories Using Many-Sorted Logic

Identifieur interne : 006288 ( Main/Exploration ); précédent : 006287; suivant : 006289

Combining Data Structures with Nonstably Infinite Theories Using Many-Sorted Logic

Auteurs : Silvio Ranise ; Christophe Ringeissen ; Calogero G. Zarba

Source :

Lecture Notes in Computer Science [ 0302-9743 ]

RBID : ISTEX:C999F91510BA36B2C64229AECD6D8034288F3847

Descripteurs français

Pascal (Inist)
- Conteneur, Exactitude programme, Modélisation, Multiensemble, Multiplicité, Programmation logique, Programme ordinateur, Structure donnée.
Wicri :
- topic : Conteneur.

English descriptors

KwdEn :
- Computer program, Container, Data structure, Logical programming, Modeling, Multiplicity, Multiset, Program correctness.

Abstract

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.

Url:

https://api.istex.fr/ark:/67375/HCB-7N6V0C23-2/fulltext.pdf

DOI: 10.1007/11559306_3

Affiliations:

Le document en format XML

<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">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>
</author>
<author><name sortKey="Ringeissen, Christophe" sort="Ringeissen, Christophe" uniqKey="Ringeissen C" first="Christophe" last="Ringeissen">Christophe Ringeissen</name>
</author>
<author><name sortKey="Zarba, Calogero G" sort="Zarba, Calogero G" uniqKey="Zarba C" first="Calogero G." last="Zarba">Calogero G. Zarba</name>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:C999F91510BA36B2C64229AECD6D8034288F3847</idno>
<date when="2005" year="2005">2005</date>
<idno type="doi">10.1007/11559306_3</idno>
<idno type="url">https://api.istex.fr/ark:/67375/HCB-7N6V0C23-2/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">002F81</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002F81</idno>
<idno type="wicri:Area/Istex/Curation">002F42</idno>
<idno type="wicri:Area/Istex/Checkpoint">001602</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001602</idno>
<idno type="wicri:doubleKey">0302-9743:2005:Ranise S:combining:data:structures</idno>
<idno type="wicri:Area/Main/Merge">006513</idno>
<idno type="wicri:source">INIST</idno>
<idno type="RBID">Pascal:05-0449866</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000509</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000529</idno>
<idno type="wicri:Area/PascalFrancis/Checkpoint">000513</idno>
<idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000513</idno>
<idno type="wicri:doubleKey">0302-9743:2005:Ranise S:combining:data:structures</idno>
<idno type="wicri:Area/Main/Merge">006650</idno>
<idno type="wicri:Area/Main/Curation">006288</idno>
<idno type="wicri:Area/Main/Exploration">006288</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">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><wicri:noCountry code="subField"> </wicri:noCountry>
</affiliation>
</author>
<author><name sortKey="Ringeissen, Christophe" sort="Ringeissen, Christophe" uniqKey="Ringeissen C" first="Christophe" last="Ringeissen">Christophe Ringeissen</name>
<affiliation><wicri:noCountry code="subField"> </wicri:noCountry>
</affiliation>
</author>
<author><name sortKey="Zarba, Calogero G" sort="Zarba, Calogero G" uniqKey="Zarba C" first="Calogero G." last="Zarba">Calogero G. Zarba</name>
<affiliation><wicri:noCountry code="subField"> </wicri:noCountry>
</affiliation>
</author>
</analytic>
<monogr></monogr>
<series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title>
<idno type="ISSN">0302-9743</idno>
<idno type="eISSN">1611-3349</idno>
<idno type="ISSN">0302-9743</idno>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><idno type="ISSN">0302-9743</idno>
</seriesStmt>
</fileDesc>
<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>Conteneur</term>
<term>Exactitude programme</term>
<term>Modélisation</term>
<term>Multiensemble</term>
<term>Multiplicité</term>
<term>Programmation logique</term>
<term>Programme ordinateur</term>
<term>Structure donnée</term>
</keywords>
<keywords scheme="Wicri" type="topic" xml:lang="fr"><term>Conteneur</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">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.</div>
</front>
</TEI>
<affiliations><list></list>
<tree><noCountry><name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name>
<name sortKey="Ringeissen, Christophe" sort="Ringeissen, Christophe" uniqKey="Ringeissen C" first="Christophe" last="Ringeissen">Christophe Ringeissen</name>
<name sortKey="Zarba, Calogero G" sort="Zarba, Calogero G" uniqKey="Zarba C" first="Calogero G." last="Zarba">Calogero G. Zarba</name>
</noCountry>
</tree>
</affiliations>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 006288 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 006288 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Exploration
   |type=    RBID
   |clé=     ISTEX:C999F91510BA36B2C64229AECD6D8034288F3847
   |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

Serveur d'exploration sur la recherche en informatique en Lorraine

Combining Data Structures with Nonstably Infinite Theories Using Many-Sorted Logic

Combining Data Structures with Nonstably Infinite Theories Using Many-Sorted Logic

Source :

Descripteurs français

English descriptors

Abstract

Links toward previous steps (curation, corpus...)

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri

	Serveur d'exploration sur la recherche en informatique en Lorraine
	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.