Adrian Francalanza ; Julian Rathke ; Vladimiro Sassone - Permission-Based Separation Logic for Message-Passing Concurrency

lmcs:772 - Logical Methods in Computer Science, September 1, 2011, Volume 7, Issue 3 - https://doi.org/10.2168/LMCS-7(3:7)2011
Permission-Based Separation Logic for Message-Passing ConcurrencyArticle

Authors: Adrian Francalanza ; Julian Rathke ; Vladimiro Sassone

We develop local reasoning techniques for message passing concurrent programs based on ideas from separation logics and resource usage analysis. We extend processes with permission- resources and define a reduction semantics for this extended language. This provides a foundation for interpreting separation formulas for message-passing concurrency. We also define a sound proof system permitting us to infer satisfaction compositionally using local, separation-based reasoning.

Comment: 47 pages

https://doi.org/10.2168/LMCS-7(3:7)2011
Source: arXiv.org:1106.5128
Volume: Volume 7, Issue 3
Published on: September 1, 2011
Imported on: September 10, 2010
Keywords: Computer Science - Logic in Computer Science, F.3.1, F.3.2, F.3.3
Licence: arXiv.org - Non-exclusive license to distribute

7 Documents citing this article

Share and export

Consultation statistics

This page has been seen 3231 times.
This article's PDF has been downloaded 478 times.