Permission-Based Separation Logic for Message-Passing Concurrency
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 sep...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2011-09-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/772/pdf |
| _version_ | 1827322947794108416 |
|---|---|
| author | Adrian Francalanza Julian Rathke Vladimiro Sassone |
| author_facet | Adrian Francalanza Julian Rathke Vladimiro Sassone |
| author_sort | Adrian Francalanza |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:36:55Z |
| format | Article |
| id | doaj.art-b5126af097624a5e992b793dea482ed9 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:36:55Z |
| publishDate | 2011-09-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-b5126af097624a5e992b793dea482ed92024-03-08T09:17:23ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742011-09-01Volume 7, Issue 310.2168/LMCS-7(3:7)2011772Permission-Based Separation Logic for Message-Passing ConcurrencyAdrian FrancalanzaJulian RathkeVladimiro SassoneWe 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.https://lmcs.episciences.org/772/pdfcomputer science - logic in computer sciencef.3.1, f.3.2, f.3.3 |
| spellingShingle | Adrian Francalanza Julian Rathke Vladimiro Sassone Permission-Based Separation Logic for Message-Passing Concurrency Logical Methods in Computer Science computer science - logic in computer science f.3.1, f.3.2, f.3.3 |
| title | Permission-Based Separation Logic for Message-Passing Concurrency |
| title_full | Permission-Based Separation Logic for Message-Passing Concurrency |
| title_fullStr | Permission-Based Separation Logic for Message-Passing Concurrency |
| title_full_unstemmed | Permission-Based Separation Logic for Message-Passing Concurrency |
| title_short | Permission-Based Separation Logic for Message-Passing Concurrency |
| title_sort | permission based separation logic for message passing concurrency |
| topic | computer science - logic in computer science f.3.1, f.3.2, f.3.3 |
| url | https://lmcs.episciences.org/772/pdf |
| work_keys_str_mv | AT adrianfrancalanza permissionbasedseparationlogicformessagepassingconcurrency AT julianrathke permissionbasedseparationlogicformessagepassingconcurrency AT vladimirosassone permissionbasedseparationlogicformessagepassingconcurrency |