Skip to Main content Skip to Navigation
Conference papers

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. As an example, we present a separation logic contract for iterators that prevents data races and concurrent modifications. Our program logic is presented in an algorithmic style: we avoid structural rules for Hoare triples and formalize logical reasoning about typed heaps by natural deduction rules and a set of sound axioms. We show that verified programs satisfy the following properties: data race freedom, absence of null-dereferences and partial correctness.
Complete list of metadata

Cited literature [27 references]  Display  Hide  Download

https://hal.inria.fr/inria-00320102
Contributor : Clément Hurlin <>
Submitted on : Wednesday, September 10, 2008 - 11:33:09 AM
Last modification on : Tuesday, December 8, 2020 - 9:48:06 AM
Long-term archiving on: : Monday, October 8, 2012 - 1:03:00 PM

File

amast.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00320102, version 1

Collections

Citation

Christian Haack, Clément Hurlin. Separation logic contracts for a Java-like language with fork/join. 12th International Conference on Algebraic Methodology and Software Technology (AMAST 2008), Jose Meseguer and Grigore Rosu, Jul 2008, Urbana, United States. ⟨inria-00320102⟩

Share

Metrics

Record views

174

Files downloads

199