Loïc Fejoz and Stephan Merz
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.
|Published in||Exploiting Concurrency Efficiently and Correctly|
|Address||Princeton États-Unis d'Amérique|