InforLorV4, Main, Exploration, bibRecordById, Pascal:04-0234385

A Separation Logic for Resource Distribution

Identifieur interne : 007B10 ( Main/Exploration ); précédent : 007B09; suivant : 007B11

A Separation Logic for Resource Distribution

Auteurs : Nicolas Biri [France] ; Didier Galmiche [France]

Source :

Lecture Notes in Computer Science [ 0302-9743 ]

RBID : ISTEX:99C8164E082799D8BFE50667C8DFA391374822BD

Descripteurs français

Pascal (Inist)
- Calcul séquent, Décidabilité, Déduction, Démonstration théorème, Développement logiciel, Informatique théorique, Localisation, Modèle logique, Monoïde, Méthode arborescente, Satisfaction, Structure donnée arborescente, Vérification modèle, Vérification programme.

English descriptors

KwdEn :
- Computer theory, Decidability, Deduction, Localization, Logic model, Monoid, Program verification, Satisfaction, Sequent calculus, Software development, Symbolic trajectory evaluation, Theorem proving, Tree data structures, Tree structured method.

Abstract

Abstract: We define a separation logic (BI-Loc) that is an extension of the Bunched Implications (BI) logic with a modality for locations. Moreover, we propose a general data structure, called resource tree, that is a node-labelled tree in which nodes contain resources that belong to a partial monoid. We also define a resource tree model for this logic that allows to reason and prove properties on resource trees. We study the decidability by model checking of the satisfaction and the validity in this separation logic and also introduce a sequent calculus for deciding validity by deduction w.r.t. a resource model. Then, we relate the separation logic and resource trees to some applications and finally define a sequent calculus for BI-Loc dedicated to a theorem proving approach.

Url:

https://api.istex.fr/ark:/67375/HCB-W6WFVBVS-W/fulltext.pdf

DOI: 10.1007/978-3-540-24597-1_3

Affiliations:

Le document en format XML

<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">A Separation Logic for Resource Distribution</title>
<author><name sortKey="Biri, Nicolas" sort="Biri, Nicolas" uniqKey="Biri N" first="Nicolas" last="Biri">Nicolas Biri</name>
</author>
<author><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:99C8164E082799D8BFE50667C8DFA391374822BD</idno>
<date when="2003" year="2003">2003</date>
<idno type="doi">10.1007/978-3-540-24597-1_3</idno>
<idno type="url">https://api.istex.fr/ark:/67375/HCB-W6WFVBVS-W/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">002387</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002387</idno>
<idno type="wicri:Area/Istex/Curation">002356</idno>
<idno type="wicri:Area/Istex/Checkpoint">001B00</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001B00</idno>
<idno type="wicri:doubleKey">0302-9743:2003:Biri N:a:separation:logic</idno>
<idno type="wicri:Area/Main/Merge">007E89</idno>
<idno type="wicri:source">INIST</idno>
<idno type="RBID">Pascal:04-0234385</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000682</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000359</idno>
<idno type="wicri:Area/PascalFrancis/Checkpoint">000729</idno>
<idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000729</idno>
<idno type="wicri:doubleKey">0302-9743:2003:Biri N:a:separation:logic</idno>
<idno type="wicri:Area/Main/Merge">007F88</idno>
<idno type="wicri:Area/Main/Curation">007B10</idno>
<idno type="wicri:Area/Main/Exploration">007B10</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">A Separation Logic for Resource Distribution</title>
<author><name sortKey="Biri, Nicolas" sort="Biri, Nicolas" uniqKey="Biri N" first="Nicolas" last="Biri">Nicolas Biri</name>
<affiliation wicri:level="4"><country xml:lang="fr">France</country>
<wicri:regionArea>LORIA – Université Henri Poincaré, 54506, Vandœuvre-lès-Nancy Cedex</wicri:regionArea>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
</placeName>
<orgName type="university">Université Henri Poincaré</orgName>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">France</country>
</affiliation>
</author>
<author><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name>
<affiliation wicri:level="4"><country xml:lang="fr">France</country>
<wicri:regionArea>LORIA – Université Henri Poincaré, 54506, Vandœuvre-lès-Nancy Cedex</wicri:regionArea>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
</placeName>
<orgName type="university">Université Henri Poincaré</orgName>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">France</country>
</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 theory</term>
<term>Decidability</term>
<term>Deduction</term>
<term>Localization</term>
<term>Logic model</term>
<term>Monoid</term>
<term>Program verification</term>
<term>Satisfaction</term>
<term>Sequent calculus</term>
<term>Software development</term>
<term>Symbolic trajectory evaluation</term>
<term>Theorem proving</term>
<term>Tree data structures</term>
<term>Tree structured method</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Calcul séquent</term>
<term>Décidabilité</term>
<term>Déduction</term>
<term>Démonstration théorème</term>
<term>Développement logiciel</term>
<term>Informatique théorique</term>
<term>Localisation</term>
<term>Modèle logique</term>
<term>Monoïde</term>
<term>Méthode arborescente</term>
<term>Satisfaction</term>
<term>Structure donnée arborescente</term>
<term>Vérification modèle</term>
<term>Vérification programme</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Abstract: We define a separation logic (BI-Loc) that is an extension of the Bunched Implications (BI) logic with a modality for locations. Moreover, we propose a general data structure, called resource tree, that is a node-labelled tree in which nodes contain resources that belong to a partial monoid. We also define a resource tree model for this logic that allows to reason and prove properties on resource trees. We study the decidability by model checking of the satisfaction and the validity in this separation logic and also introduce a sequent calculus for deciding validity by deduction w.r.t. a resource model. Then, we relate the separation logic and resource trees to some applications and finally define a sequent calculus for BI-Loc dedicated to a theorem proving approach.</div>
</front>
</TEI>
<affiliations><list><country><li>France</li>
</country>
<region><li>Grand Est</li>
<li>Lorraine (région)</li>
</region>
<settlement><li>Vandœuvre-lès-Nancy</li>
</settlement>
<orgName><li>Université Henri Poincaré</li>
</orgName>
</list>
<tree><country name="France"><region name="Grand Est"><name sortKey="Biri, Nicolas" sort="Biri, Nicolas" uniqKey="Biri N" first="Nicolas" last="Biri">Nicolas Biri</name>
</region>
<name sortKey="Biri, Nicolas" sort="Biri, Nicolas" uniqKey="Biri N" first="Nicolas" last="Biri">Nicolas Biri</name>
<name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name>
<name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name>
</country>
</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 007B10 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 007B10 | 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:99C8164E082799D8BFE50667C8DFA391374822BD
   |texte=   A Separation Logic for Resource Distribution
}}

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

A Separation Logic for Resource Distribution

A Separation Logic for Resource Distribution

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.