A Separation Logic for Resource Distribution
Identifieur interne : 003945 ( Crin/Corpus ); précédent : 003944; suivant : 003946A Separation Logic for Resource Distribution
Auteurs : Nicolas Biri ; Didier GalmicheSource :
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.
Links to Exploration step
CRIN:biri03aLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="189">A Separation Logic for Resource Distribution</title></titleStmt><publicationStmt><idno type="RBID">CRIN:biri03a</idno><date when="2003" year="2003">2003</date><idno type="wicri:Area/Crin/Corpus">003945</idno></publicationStmt><sourceDesc><biblStruct><analytic><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></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>decidability</term><term>model checking</term><term>resources</term><term>separation logics</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en" wicri:score="2175">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><BibTex type="inproceedings"><ref>biri03a</ref><crinnumber>A03-R-211</crinnumber><category>3</category><equipe>TYPES</equipe><author><e>Biri, Nicolas</e><e>Galmiche, Didier</e></author><title>A Separation Logic for Resource Distribution</title><booktitle>{23rd Conference on Foundations of Software Technology and Theoretical Computer Science 2003- FSTTCS'03, Mumbai, India}</booktitle><year>2003</year><series>Lecture Notes in Computer Science</series><month>Dec</month><publisher>Springer Verlag</publisher><keywords><e>separation logics</e><e>resources</e><e>decidability</e><e>model checking</e></keywords><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.</abstract></BibTex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Crin/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 003945 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Crin/Corpus/biblio.hfd -nk 003945 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Crin
|étape= Corpus
|type= RBID
|clé= CRIN:biri03a
|texte= A Separation Logic for Resource Distribution
}}
| This area was generated with Dilib version V0.6.33. |  |