A Separation Logic for Resource Distribution

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 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.
Type de document :
Communication dans un congrès
Paritosh K. Pandya and Jaikumar Radhakrishnan. 23rd Conference on Foundations of Software Technology and Theoretical Computer Science 2003 - FST TCS'03, 2003, Mumbai/India, Springer Verlag, 2914, pp.23-37, 2003, Lecture Notes in Computer Science. 〈10.1007/b94618〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00099555
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 09:38:41
Dernière modification le : mardi 24 avril 2018 - 13:34:49

Identifiants

Collections

Citation

Nicolas Biri, Didier Galmiche. A Separation Logic for Resource Distribution. Paritosh K. Pandya and Jaikumar Radhakrishnan. 23rd Conference on Foundations of Software Technology and Theoretical Computer Science 2003 - FST TCS'03, 2003, Mumbai/India, Springer Verlag, 2914, pp.23-37, 2003, Lecture Notes in Computer Science. 〈10.1007/b94618〉. 〈inria-00099555〉

Partager

Métriques

Consultations de la notice

52