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.
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
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>
