I was a PhD student at INRIA Cambium team for two years under the supervision of Luc Maranget and Jean-Marie Madiot.
We were trying to find a generic condition on axiomatic memory models that would imply the strong DRF-SC guarantee. We were aiming to prove this generic condition correct in the Coq proof assistant.