Towards automatic proofs of lock-free algorithms

Loïc Fejoz 1 Stephan Merz 1
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : The verification of lock-free data structures has traditionally been considered as difficult. We propose a formal model for describing such algorithms. The verification conditions generated from this model can often be handled by automatic theorem provers.
Type de document :
Communication dans un congrès
Exploiting Concurrency Efficiently and Correctly, Jul 2008, Princeton, United States. 2008
Liste complète des métadonnées


https://hal.inria.fr/inria-00285752
Contributeur : Loïc Fejoz <>
Soumis le : vendredi 6 juin 2008 - 11:12:57
Dernière modification le : mardi 13 décembre 2016 - 15:40:27
Document(s) archivé(s) le : vendredi 28 septembre 2012 - 15:36:11

Fichier

ec2-08-fejoz-merz.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00285752, version 1

Collections

Citation

Loïc Fejoz, Stephan Merz. Towards automatic proofs of lock-free algorithms. Exploiting Concurrency Efficiently and Correctly, Jul 2008, Princeton, United States. 2008. <inria-00285752>

Partager

Métriques

Consultations de
la notice

173

Téléchargements du document

96