Permission-Based Separation Logic for Message-Passing Concurrency
Logic in Computer Science
2015-07-01 v3
Abstract
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.
Cite
@article{arxiv.1106.5128,
title = {Permission-Based Separation Logic for Message-Passing Concurrency},
author = {Adrian Francalanza and Julian Rathke and Vladimiro Sassone},
journal= {arXiv preprint arXiv:1106.5128},
year = {2015}
}
Comments
47 pages