Lindsay Groves: Verifying Michael and Scott's Lock-Free Queue Algorithm using Trace Reduction. CATS 2008: 133-142