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.
Type de document :
Communication dans un congrès
Springer-Verlag. 12th International Conference on Algebraic Methodology and Software Technology (AMAST 2008), Jul 2008, Urbana, United States. 5140, 2008, Lecture Notes in Computer Science
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00320102
Contributeur : Clément Hurlin <>
Soumis le : mercredi 10 septembre 2008 - 11:33:09
Dernière modification le : samedi 27 janvier 2018 - 01:30:48
Document(s) archivé(s) le : lundi 8 octobre 2012 - 13:03:00

Fichier

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

Identifiants

  • HAL Id : inria-00320102, version 1

Collections

Citation

Christian Haack, Clément Hurlin. Separation logic contracts for a Java-like language with fork/join. Springer-Verlag. 12th International Conference on Algebraic Methodology and Software Technology (AMAST 2008), Jul 2008, Urbana, United States. 5140, 2008, Lecture Notes in Computer Science. 〈inria-00320102〉

Partager

Métriques

Consultations de la notice

124

Téléchargements de fichiers

103