A separation logic for resource distribution
Identifieur interne : 000729 ( PascalFrancis/Checkpoint ); précédent : 000728; suivant : 000730A separation logic for resource distribution
Auteurs : Nicolas Biri [France] ; Didier Galmiche [France]Source :
- Lecture notes in computer science [ 0302-9743 ] ; 2003.
Descripteurs français
- Pascal (Inist)
English descriptors
- KwdEn :
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.
Affiliations:
Links toward previous steps (curation, corpus...)
Links to Exploration step
Pascal:04-0234385Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">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"><inist:fA14 i1="01"><s1>LORIA - Université Henri Poincaré</s1><s2>54506 Vandœuvre-lès-Nancy </s2><s3>FRA</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ></inist:fA14><country>France</country><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></author><author><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name><affiliation wicri:level="4"><inist:fA14 i1="01"><s1>LORIA - Université Henri Poincaré</s1><s2>54506 Vandœuvre-lès-Nancy </s2><s3>FRA</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ></inist:fA14><country>France</country><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></author></titleStmt><publicationStmt><idno type="wicri:source">INIST</idno><idno type="inist">04-0234385</idno><date when="2003">2003</date><idno type="stanalyst">PASCAL 04-0234385 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></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">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"><inist:fA14 i1="01"><s1>LORIA - Université Henri Poincaré</s1><s2>54506 Vandœuvre-lès-Nancy </s2><s3>FRA</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ></inist:fA14><country>France</country><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></author><author><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name><affiliation wicri:level="4"><inist:fA14 i1="01"><s1>LORIA - Université Henri Poincaré</s1><s2>54506 Vandœuvre-lès-Nancy </s2><s3>FRA</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ></inist:fA14><country>France</country><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></author></analytic><series><title level="j" type="main">Lecture notes in computer science</title><idno type="ISSN">0302-9743</idno><imprint><date when="2003">2003</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>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>Informatique théorique</term><term>Développement logiciel</term><term>Localisation</term><term>Structure donnée arborescente</term><term>Décidabilité</term><term>Vérification programme</term><term>Démonstration théorème</term><term>Méthode arborescente</term><term>Monoïde</term><term>Modèle logique</term><term>Satisfaction</term><term>Déduction</term><term>Vérification modèle</term><term>Calcul séquent</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">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><inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0302-9743</s0></fA01><fA05><s2>2914</s2></fA05><fA08 i1="01" i2="1" l="ENG"><s1>A separation logic for resource distribution</s1></fA08><fA09 i1="01" i2="1" l="ENG"><s1>FST TCS 2003 : foundations of software technology and theoretical computer science : Mumbai, 15-17 December 2003</s1></fA09><fA11 i1="01" i2="1"><s1>BIRI (Nicolas)</s1></fA11><fA11 i1="02" i2="1"><s1>GALMICHE (Didier)</s1></fA11><fA12 i1="01" i2="1"><s1>PANDYA (Paritosh K.)</s1><s9>ed.</s9></fA12><fA12 i1="02" i2="1"><s1>RADHAKRISHNAN (Jaikumar)</s1><s9>ed.</s9></fA12><fA14 i1="01"><s1>LORIA - Université Henri Poincaré</s1><s2>54506 Vandœuvre-lès-Nancy </s2><s3>FRA</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ></fA14><fA20><s1>23-37</s1></fA20><fA21><s1>2003</s1></fA21><fA23 i1="01"><s0>ENG</s0></fA23><fA26 i1="01"><s0>3-540-20680-9</s0></fA26><fA43 i1="01"><s1>INIST</s1><s2>16343</s2><s5>354000117812920030</s5></fA43><fA44><s0>0000</s0><s1>© 2004 INIST-CNRS. All rights reserved.</s1></fA44><fA45><s0>16 ref.</s0></fA45><fA47 i1="01" i2="1"><s0>04-0234385</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 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.</s0></fC01><fC02 i1="01" i2="X"><s0>001D02A01</s0></fC02><fC03 i1="01" i2="X" l="FRE"><s0>Informatique théorique</s0><s5>01</s5></fC03><fC03 i1="01" i2="X" l="ENG"><s0>Computer theory</s0><s5>01</s5></fC03><fC03 i1="01" i2="X" l="SPA"><s0>Informática teórica</s0><s5>01</s5></fC03><fC03 i1="02" i2="X" l="FRE"><s0>Développement logiciel</s0><s5>02</s5></fC03><fC03 i1="02" i2="X" l="ENG"><s0>Software development</s0><s5>02</s5></fC03><fC03 i1="02" i2="X" l="SPA"><s0>Desarrollo logicial</s0><s5>02</s5></fC03><fC03 i1="03" i2="X" l="FRE"><s0>Localisation</s0><s5>09</s5></fC03><fC03 i1="03" i2="X" l="ENG"><s0>Localization</s0><s5>09</s5></fC03><fC03 i1="03" i2="X" l="SPA"><s0>Localización</s0><s5>09</s5></fC03><fC03 i1="04" i2="3" l="FRE"><s0>Structure donnée arborescente</s0><s5>10</s5></fC03><fC03 i1="04" i2="3" l="ENG"><s0>Tree data structures</s0><s5>10</s5></fC03><fC03 i1="05" i2="X" l="FRE"><s0>Décidabilité</s0><s5>11</s5></fC03><fC03 i1="05" i2="X" l="ENG"><s0>Decidability</s0><s5>11</s5></fC03><fC03 i1="05" i2="X" l="SPA"><s0>Decidibilidad</s0><s5>11</s5></fC03><fC03 i1="06" i2="X" l="FRE"><s0>Vérification programme</s0><s5>12</s5></fC03><fC03 i1="06" i2="X" l="ENG"><s0>Program verification</s0><s5>12</s5></fC03><fC03 i1="06" i2="X" l="SPA"><s0>Verificación programa</s0><s5>12</s5></fC03><fC03 i1="07" i2="X" l="FRE"><s0>Démonstration théorème</s0><s5>13</s5></fC03><fC03 i1="07" i2="X" l="ENG"><s0>Theorem proving</s0><s5>13</s5></fC03><fC03 i1="07" i2="X" l="SPA"><s0>Demostración teorema</s0><s5>13</s5></fC03><fC03 i1="08" i2="X" l="FRE"><s0>Méthode arborescente</s0><s5>18</s5></fC03><fC03 i1="08" i2="X" l="ENG"><s0>Tree structured method</s0><s5>18</s5></fC03><fC03 i1="08" i2="X" l="SPA"><s0>Método arborescente</s0><s5>18</s5></fC03><fC03 i1="09" i2="X" l="FRE"><s0>Monoïde</s0><s5>19</s5></fC03><fC03 i1="09" i2="X" l="ENG"><s0>Monoid</s0><s5>19</s5></fC03><fC03 i1="09" i2="X" l="SPA"><s0>Monoide</s0><s5>19</s5></fC03><fC03 i1="10" i2="X" l="FRE"><s0>Modèle logique</s0><s5>20</s5></fC03><fC03 i1="10" i2="X" l="ENG"><s0>Logic model</s0><s5>20</s5></fC03><fC03 i1="10" i2="X" l="SPA"><s0>Modelo lógico</s0><s5>20</s5></fC03><fC03 i1="11" i2="X" l="FRE"><s0>Satisfaction</s0><s5>21</s5></fC03><fC03 i1="11" i2="X" l="ENG"><s0>Satisfaction</s0><s5>21</s5></fC03><fC03 i1="11" i2="X" l="SPA"><s0>Satisfacción</s0><s5>21</s5></fC03><fC03 i1="12" i2="X" l="FRE"><s0>Déduction</s0><s5>22</s5></fC03><fC03 i1="12" i2="X" l="ENG"><s0>Deduction</s0><s5>22</s5></fC03><fC03 i1="12" i2="X" l="SPA"><s0>Deducción</s0><s5>22</s5></fC03><fC03 i1="13" i2="X" l="FRE"><s0>Vérification modèle</s0><s4>CD</s4><s5>96</s5></fC03><fC03 i1="13" i2="X" l="ENG"><s0>Symbolic trajectory evaluation</s0><s4>CD</s4><s5>96</s5></fC03><fC03 i1="14" i2="X" l="FRE"><s0>Calcul séquent</s0><s4>CD</s4><s5>97</s5></fC03><fC03 i1="14" i2="X" l="ENG"><s0>Sequent calculus</s0><s4>CD</s4><s5>97</s5></fC03><fC03 i1="14" i2="X" l="SPA"><s0>Càlculo sequente</s0><s4>CD</s4><s5>97</s5></fC03><fN21><s1>152</s1></fN21><fN82><s1>OTO</s1></fN82></pA><pR><fA30 i1="01" i2="1" l="ENG"><s1>Foundations of software technology and theoretical computer science. Conference</s1><s2>23</s2><s3>Mumbai IND</s3><s4>2003-12-15</s4></fA30></pR></standard></inist><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="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/PascalFrancis/Checkpoint
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000729 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Checkpoint/biblio.hfd -nk 000729 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= PascalFrancis
|étape= Checkpoint
|type= RBID
|clé= Pascal:04-0234385
|texte= A separation logic for resource distribution
}}
| This area was generated with Dilib version V0.6.33. |  |