A Separation Logic for the Pi-calculus. Turon, A. & Wand, M. July 2009. unpublished

Paper abstract bibtex

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.

@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"]}