I am a PhD student at INRIA Cambium team under the supervision of Luc Maranget and Jean-Marie Madiot.

We're trying to find a generic condition on axiomatic memory models that would imply the DRF-SC guarantee. We are aiming to prove this generic condition correct in the Coq proof assistant.

You can contact me at : quentin dot ladeveze at inria.fr