Towards automatic proofs of lock-free algorithms
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.
Origin : Files produced by the author(s)
Loading...