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.
Type de document :
Rapport
[Technical Report] RR-6430, INRIA. 2008, pp.101
Liste complète des métadonnées

Littérature citée [37 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00218114
Contributeur : Clément Hurlin <>
Soumis le : mercredi 27 février 2008 - 11:05:12
Dernière modification le : jeudi 11 janvier 2018 - 16:25:42
Document(s) archivé(s) le : vendredi 24 septembre 2010 - 11:08:50

Fichiers

techrep.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

116

Téléchargements de fichiers

165