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 Contributor : Loïc FejozConnect in order to contact the contributor Submitted on : Friday, June 6, 2008 - 11:12:57 AM Last modification on : Friday, February 4, 2022 - 3:32:22 AM Long-term archiving on: : Friday, September 28, 2012 - 3:36:11 PM
Loïc Fejoz, Stephan Merz. Towards automatic proofs of lock-free algorithms. Exploiting Concurrency Efficiently and Correctly, Jul 2008, Princeton, United States. ⟨inria-00285752⟩