Towards automatic proofs of lock-free algorithms
Résumé
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.
Origine : Fichiers produits par l'(les) auteur(s)
Loading...