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 sepa...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
2011-09-01.
|
| Subjects: | |
| Online Access: | Get fulltext Get fulltext |
| Summary: | 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. |
|---|