A Separation Logic for the Pi-calculus. Turon, A. & Wand, M. July 2009. unpublished
A Separation Logic for the Pi-calculus [pdf]Paper  abstract   bibtex   
Reasoning about concurrent processes requires distinguishing communication from interference, and is especially difficult when the means of interaction change over time. We present a new logic for the pi-calculus that combines temporal and separation logic, and treats channels as resources that can be gained and lost by processes. The resource model provides a lightweight way to constrain interference. By interpreting process terms as formulas, our logic directly supports compositional reasoning.

Downloads: 0