Characterizing Provability in BI ’s Pointer Logic Through Resource Graphs
Identifieur interne : 002D51 ( Istex/Curation ); précédent : 002D50; suivant : 002D52Characterizing Provability in BI ’s Pointer Logic Through Resource Graphs
Auteurs : Didier Galmiche [France] ; Daniel Méry [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: We propose a characterization of provability in BI’s Pointer Logic (PL) that is based on semantic structures called resource graphs. This logic has been defined for reasoning about mutable data structures and results about models and verification have been already provided. Here, we define resource graphs that capture PL models by considering heaps as resources and by using a labelling process. We study provability in PL from a new calculus that builds such graphs from which proofs or countermodels can be generated. Properties of soundness and completeness are proved and the countermodel generation is studied.
Url:
DOI: 10.1007/11591191_32
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: Pour aller vers cette notice dans l'étape Curation :002D88
Links to Exploration step
ISTEX:C1B5391D5C9CA108ECDEC7EE18C205AE779B3237Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Characterizing Provability in BI ’s Pointer Logic Through Resource Graphs</title>
<author><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name>
<affiliation wicri:level="1"><mods:affiliation>LORIA – Université Henri Poincaré, Campus Scientifique, BP 239, Vandœuvre-lès-Nancy, France</mods:affiliation>
<country xml:lang="fr">France</country>
<wicri:regionArea>LORIA – Université Henri Poincaré, Campus Scientifique, BP 239, Vandœuvre-lès-Nancy</wicri:regionArea>
</affiliation>
</author>
<author><name sortKey="Mery, Daniel" sort="Mery, Daniel" uniqKey="Mery D" first="Daniel" last="Méry">Daniel Méry</name>
<affiliation wicri:level="1"><mods:affiliation>LORIA – Université Henri Poincaré, Campus Scientifique, BP 239, Vandœuvre-lès-Nancy, France</mods:affiliation>
<country xml:lang="fr">France</country>
<wicri:regionArea>LORIA – Université Henri Poincaré, Campus Scientifique, BP 239, Vandœuvre-lès-Nancy</wicri:regionArea>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:C1B5391D5C9CA108ECDEC7EE18C205AE779B3237</idno>
<date when="2005" year="2005">2005</date>
<idno type="doi">10.1007/11591191_32</idno>
<idno type="url">https://api.istex.fr/ark:/67375/HCB-WJQK55N7-H/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">002D88</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002D88</idno>
<idno type="wicri:Area/Istex/Curation">002D51</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Characterizing Provability in <hi rend="SansSerif">BI</hi>
’s Pointer Logic Through Resource Graphs</title>
<author><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name>
<affiliation wicri:level="1"><mods:affiliation>LORIA – Université Henri Poincaré, Campus Scientifique, BP 239, Vandœuvre-lès-Nancy, France</mods:affiliation>
<country xml:lang="fr">France</country>
<wicri:regionArea>LORIA – Université Henri Poincaré, Campus Scientifique, BP 239, Vandœuvre-lès-Nancy</wicri:regionArea>
</affiliation>
</author>
<author><name sortKey="Mery, Daniel" sort="Mery, Daniel" uniqKey="Mery D" first="Daniel" last="Méry">Daniel Méry</name>
<affiliation wicri:level="1"><mods:affiliation>LORIA – Université Henri Poincaré, Campus Scientifique, BP 239, Vandœuvre-lès-Nancy, France</mods:affiliation>
<country xml:lang="fr">France</country>
<wicri:regionArea>LORIA – Université Henri Poincaré, Campus Scientifique, BP 239, Vandœuvre-lès-Nancy</wicri:regionArea>
</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></textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Abstract: We propose a characterization of provability in BI’s Pointer Logic (PL) that is based on semantic structures called resource graphs. This logic has been defined for reasoning about mutable data structures and results about models and verification have been already provided. Here, we define resource graphs that capture PL models by considering heaps as resources and by using a labelling process. We study provability in PL from a new calculus that builds such graphs from which proofs or countermodels can be generated. Properties of soundness and completeness are proved and the countermodel generation is studied.</div>
</front>
</TEI>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 002D51 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Curation/biblio.hfd -nk 002D51 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien |wiki= Wicri/Lorraine |area= InforLorV4 |flux= Istex |étape= Curation |type= RBID |clé= ISTEX:C1B5391D5C9CA108ECDEC7EE18C205AE779B3237 |texte= Characterizing Provability in BI ’s Pointer Logic Through Resource Graphs }}
![]() | This area was generated with Dilib version V0.6.33. | ![]() |