Towards automatic proofs of lock-free algorithms

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.

In  Exploiting Concurrency Efficiently and Correctly

Details

TypeInproceedings
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