A. Ahmed, A. W. Appel, C. D. Richards, K. N. Swadi, G. Tan et al., Semantic foundations for typed assembly languages, TOPLAS, vol.32, pp.1-67, 2010.

M. Batty, S. Owens, S. Sarkar, P. Sewell, and T. Weber, Mathematizing C++ Concurrency, POPL, pp.55-66, 2011.

-. Hans, B. Boehm, and . Demsky, Outlawing ghosts: Avoiding out-of-thin-air results, MSPC, 2014.

R. Bornat, C. Calcagno, P. W. O'hearn, and M. J. Parkinson, Permission accounting in separation logic, pp.259-270, 2005.

J. Boyland, Checking interference with fractional permissions, SAS (LNCS), 2003.

D. Chase and Y. Lev, Dynamic circular work-stealing deque, SPAA. 21-28, 2005.

H. Dang, J. Jourdan, J. Kaiser, and D. Dreyer, Appendix and Coq development accompanying this paper, 2019.

S. Doherty, B. Dongol, H. Wehrheim, and J. Derrick, Verifying C11 Programs Operationally, PPoPP, pp.355-365, 2019.

M. Doko and V. Vafeiadis, A Program Logic for C11 Memory Fences, VMCAI (LNCS), pp.413-430, 2016.

M. Doko and V. Vafeiadis, Tackling Real-Life Relaxed Concurrency with FSL++, ESOP, 2017.

D. Dreyer, Local Reasoning for Storable Locks and Threads, RustBelt project webpage, pp.19-37, 2007.

M. He, V. Vafeiadis, S. Qin, and J. F. Ferreira, GPS+: Reasoning About Fences and Relaxed Atomics, International Journal of Parallel Programming, vol.46, pp.1157-1183, 2018.

A. Hobor, A. W. Appel, and F. Z. Nardelli, Oracle Semantics for Concurrent Separation Logic, ESOP, pp.353-367, 2008.

J. Jourdan, Insufficient synchronization in Arc::get_mut, 2018.

R. Jung, J. Jourdan, R. Krebbers, and D. Dreyer, RustBelt: Securing the Foundations of the Rust Programming Language, Article, vol.2, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01633165

R. Jung, R. Krebbers, and J. Jourdan, Iris from the Ground Up: A Modular Foundation for Higher-Order Concurrent Separation Logic, Journal of Functional Programming, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01945446

J. Kaiser, H. Dang, D. Dreyer, O. Lahav, and V. Vafeiadis, Strong Logic for Weak Memory: Reasoning about Release-Acquire Consistency in Iris, ECOOP (LIPIcs), vol.17, p.29, 2017.

J. Kang, C. Hur, and O. Lahav, Viktor Vafeiadis, and Derek Dreyer. 2017. A Promising Semantics for Relaxedmemory Concurrency, POPL. ACM, pp.175-189

S. Klabnik and C. Nichols, Interactive Proofs in Higher-Order Concurrent Separation Logic, Amin Timany, and Lars Birkedal, 2017.

O. Lahav, V. Vafeiadis, J. Kang, C. Hur, and D. Dreyer, Repairing sequential consistency in C/C++11, PLDI, 2017.

L. Lamport, How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs, IEEE Trans. Computers, vol.28, pp.690-691, 1979.

A. Podkopaev, I. Sergey, and A. Nanevski, Operational Aspects of C/C++ Concurrency, 2016.

J. C. Reynolds, Separation logic: A logic for shared mutable data structures, LICS, 2002.

K. Svendsen, J. Pichon-pharabod, and M. Doko, A Separation Logic for a Promising Semantics, ESOP, pp.357-384, 2018.

J. Tassarotti, D. Dreyer, and V. Vafeiadis, Verifying read-copy-update in a logic for weak memory, 2015.

A. Turon, Crossbeam: Support for concurrent and parallel programming, 2016.

A. Turon, V. Vafeiadis, and D. Dreyer, GPS: Navigating Weak Memory with Ghosts, Protocols, and Separation, OOPSLA. ACM, pp.691-707, 2014.

V. Vafeaidis and C. Narayan, Relaxed Separation Logic: A Program Logic for C11 Concurrency, OOPSLA, 2013.