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 : jeudi 11 janvier 2018 - 06:19:52
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〉
