HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Resource Tree and Logics for Distribution - abstract

Nicolas Biri 1 Didier Galmiche 1
1 TYPES - Logic, proof Theory and Programming
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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. This model is extended with quantifications on locations and paths and (un)decidability results are given for such extensions. Moreover, we relate the logics and the models to the specification and verification of properties of XML and semi-structured data.
Document type :
Conference papers
Complete list of metadata

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 10:13:41 AM
Last modification on : Friday, February 26, 2021 - 3:28:08 PM


  • HAL Id : inria-00100046, version 1



Nicolas Biri, Didier Galmiche. Resource Tree and Logics for Distribution - abstract. 2nd APPSEM II Workshop - APPSEM'04, Institute of Cybernetics, 2004, Tallinn/Estonia. ⟨inria-00100046⟩



Record views