We use ConcurrentIMP to model Schism, a state-of-the-art real-time garbage collection scheme for weak memory, and show that it is safe on x86-TSO. This development accompanies the PLDI 2015 paper of the same name.
@incollection{Gammie+2015AFP,
author = {Gammie, Peter and Hosking, Antony L. and Engelhardt, Kai},
title = {Relaxing Safely: Verified On-the-Fly Garbage Collection for
x86-TSO},
booktitle = {Archive of Formal Proofs},
series = {AFP},
month = {April},
year = {2015},
url = {http://afp.sourceforge.net/entries/ConcurrentGC.shtml}
}