Separation logic contracts for a Java-like language with fork/join - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2008

Separation logic contracts for a Java-like language with fork/join

Christian Haack
  • Fonction : Auteur
  • PersonId : 846315

Résumé

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.
Fichier principal
Vignette du fichier
amast.pdf (158.7 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00320102 , version 1 (10-09-2008)

Identifiants

  • HAL Id : inria-00320102 , version 1

Citer

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⟩

Collections

INRIA INRIA2 ANR
79 Consultations
101 Téléchargements

Partager

Gmail Facebook X LinkedIn More