Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Towards automatic proofs of lock-free algorithms

Loïc Fejoz and Stephan Merz

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.

Details

Publication typeInproceedings
Published inExploiting Concurrency Efficiently and Correctly
URLhttp://hal.inria.fr/inria-00285752/PDF/ec2-08-fejoz-merz.pdf
AddressPrinceton États-Unis d'Amérique
> Publications > Towards automatic proofs of lock-free algorithms