Shared memory consistency models: a tutorial, Computer, vol.29, issue.12, pp.66-76, 1995. ,
DOI : 10.1109/2.546611
A Shared Memory Poetics, 2010. ,
Testing for Weak Memory Model Exploration ,
Stability in Weak Memory Models, CAV, 2011. ,
DOI : 10.1007/978-3-540-30482-1_11
URL : https://hal.archives-ouvertes.fr/hal-01100806
Fences in Weak Memory Models, 2010. ,
DOI : 10.1007/978-3-642-14295-6_25
URL : https://hal.archives-ouvertes.fr/hal-01100859
Coq'Art, EATCS Texts in Theoretical Computer Science ,
URL : https://hal.archives-ouvertes.fr/hal-00344237
CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates, Mathematical Structures in Computer Science, vol.37, issue.04 ,
DOI : 10.1016/S0890-5401(03)00011-7
URL : https://hal.archives-ouvertes.fr/inria-00543157
Memory Model Safety of Programs, 2008. ,
Specification and Verification of ARM Hardware and Software, Design and Verification of Microprocessor Systems for High- Assurance Applications, 2010. ,
DOI : 10.1007/978-1-4419-1539-9_8
A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture, 2010. ,
DOI : 10.1007/978-3-642-14052-5_18
An introduction to small scale reflection in Coq, Journal of Formalized Reasoning, vol.3, pp.95-152, 2010. ,
URL : https://hal.archives-ouvertes.fr/inria-00515548
A small scale reflection extension for the Coq system ,
URL : https://hal.archives-ouvertes.fr/inria-00258384
How to make a correct multiprocess program execute correctly on a multiprocessor, IEEE Transactions on Computers, vol.46, issue.7, pp.779-782, 1979. ,
DOI : 10.1109/12.599898
Formal certification of a compiler back-end, or: programming a compiler with a proof assistant, POPL, 2006. ,
URL : https://hal.archives-ouvertes.fr/inria-00000963
The Java Memory Model, POPL, 2005. ,
DOI : 10.1145/1047659.1040336
Verified LISP Implementations on ARM,??x86??and??PowerPC, TPHOL 09 ,
DOI : 10.1007/978-3-540-71067-7_6
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.154.5045
Reasoning about the Implementation of Concurrency Abstractions on x86-TSO, 2010. ,
DOI : 10.1007/978-3-642-14107-2_23
A Better x86 Memory Model, p.86, 2009. ,
Acyclic Preferences and Existence of Sequential Nash Equilibria: A Formal and Constructive Equivalence, TPHOLs, 2009. ,
The Semantics of x86-CC Multiprocessor Machine Code, POPL, 2009. ,
Relaxedmemory concurrency and verified compilation, POPL, 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-00907801