A Separation Logic for the Pi-calculus. Turon, A. & Wand, M. July 2009. unpublishedPaper 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.
@Unpublished{TuronWand-09,
author = {Aaron Turon and Mitchell Wand},
title = {A Separation Logic for the Pi-calculus},
note = {unpublished},
abstract = {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.},
URL = ftpdir # {turon-wand-09.pdf},
source = {~/papers/popl-10},
OPTkey = {},
month = jul,
year = {2009},
OPTannote = {}
}
Downloads: 0
{"_id":"cgjbNEkw5t4o2JaA9","bibbaseid":"turon-wand-aseparationlogicforthepicalculus-2009","downloads":0,"creationDate":"2017-04-23T20:31:12.635Z","title":"A Separation Logic for the Pi-calculus","author_short":["Turon, A.","Wand, M."],"year":2009,"bibtype":"unpublished","biburl":"http://www.ccs.neu.edu/home/wand/Bibliography.bib","bibdata":{"bibtype":"unpublished","type":"unpublished","author":[{"firstnames":["Aaron"],"propositions":[],"lastnames":["Turon"],"suffixes":[]},{"firstnames":["Mitchell"],"propositions":[],"lastnames":["Wand"],"suffixes":[]}],"title":"A Separation Logic for the Pi-calculus","note":"unpublished","abstract":"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.","url":"ftp://ftp.ccs.neu.edu/pub/people/wand/papers/turon-wand-09.pdf","source":"~/papers/popl-10","optkey":"","month":"July","year":"2009","optannote":"","bibtex":"@Unpublished{TuronWand-09,\n author = \t {Aaron Turon and Mitchell Wand},\n title = \t {A Separation Logic for the Pi-calculus},\n note = \t {unpublished},\n abstract = {Reasoning about concurrent processes requires distinguishing communication\nfrom interference, and is especially difficult when the\nmeans of interaction change over time. We present a new logic for\nthe pi-calculus that combines temporal and separation logic, and\ntreats channels as resources that can be gained and lost by processes.\nThe resource model provides a lightweight way to constrain\ninterference. By interpreting process terms as formulas, our logic\ndirectly supports compositional reasoning.},\n URL = ftpdir # {turon-wand-09.pdf},\n source = {~/papers/popl-10},\n OPTkey = \t {},\n month =\t jul,\n year =\t {2009},\n OPTannote = \t {}\n}\n\n","author_short":["Turon, A.","Wand, M."],"key":"TuronWand-09","id":"TuronWand-09","bibbaseid":"turon-wand-aseparationlogicforthepicalculus-2009","role":"author","urls":{"Paper":"ftp://ftp.ccs.neu.edu/pub/people/wand/papers/turon-wand-09.pdf"},"downloads":0,"html":""},"search_terms":["separation","logic","calculus","turon","wand"],"keywords":[],"authorIDs":["58fd0f10bfc623c939000018"],"dataSources":["zM8mNPR4ZkAHKtvDs"]}