Skip to Main content Skip to Navigation
Reports

Separation Logic Contracts for a Java-like Language with Fork/Join

Abstract : We adapt a variant of permission-accounting separation logic to a concurrent Java-like language with fork/join. To support both concurrent reads and information hiding, we combine fractional permissions with abstract predicates. We present a separation logic contract for iterators that prevents data races and concurrent modifications. Our program logic is presented in an algorithmic style, based on a proof-theoretical logical consequence. We show that verified programs satisfy the following properties: data race freedom, absence of null-dereferences and partial correctness.
Document type :
Reports
Complete list of metadata

Cited literature [37 references]  Display  Hide  Download

https://hal.inria.fr/inria-00218114
Contributor : Clément Hurlin Connect in order to contact the contributor
Submitted on : Wednesday, February 27, 2008 - 11:05:12 AM
Last modification on : Friday, February 4, 2022 - 3:14:46 AM
Long-term archiving on: : Friday, September 24, 2010 - 11:08:50 AM

Files

techrep.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00218114, version 4

Collections

Citation

Christian Haack, Clément Hurlin. Separation Logic Contracts for a Java-like Language with Fork/Join. [Technical Report] RR-6430, INRIA. 2008, pp.101. ⟨inria-00218114v4⟩

Share

Metrics

Record views

79

Files downloads

325