J. Alglave and L. Maranget, The diy tool

J. Alglave, L. Maranget, S. Sarkar, and P. Sewell, Fences in Weak Memory Models, Proc. CAV, 2010.
DOI : 10.1007/978-3-642-14295-6_25
URL : https://hal.archives-ouvertes.fr/hal-01100859

J. Alglave, L. Maranget, S. Sarkar, and P. Sewell, Litmus: Running Tests against Hardware, Proceedings of TACAS 2011: the 17th international conference on Tools and Algorithms for the Construction and Analysis of Systems, pp.41-44, 2011.
DOI : 10.1145/1785414.1785443
URL : https://hal.archives-ouvertes.fr/hal-01100851

J. Alglave, L. Maranget, and M. Tautschnig, Herding Cats: Modelling , Simulation, Testing, and Data Mining for Weak Memory, ACM TOPLAS, vol.367, issue.2, pp.1-7, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01081364

R. M. Amadio, N. Ayache, F. Bobot, J. Boender, B. Campbell et al., Certified complexity (cerco) In Foundational and Practical Aspects of Resource Analysis -Third International Workshop, FOPARA 2013, pp.1-18, 2013.

W. W. Collier, Reasoning about parallel architectures, 1992.

J. A. Dias and N. Ramsey, Automatically generating instruction selectors using declarative machine descriptions, Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '10, pp.403-416

A. C. Fox, Directions in ISA Specification, Interactive Theorem Proving ? Third International Conference. Proceedings, pp.338-344, 2012.
DOI : 10.1007/978-3-642-32347-8_23

S. Goel, W. A. Hunt, M. Kaufmann, and S. Ghosh, Simulation and formal verification of x86 machine-code programs that make system calls, 2014 Formal Methods in Computer-Aided Design (FMCAD), pp.91-109
DOI : 10.1109/FMCAD.2014.6987600

K. E. Gray, G. Kerneis, D. Mulligan, C. Pulte, S. Sarkar et al., An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors, Proceedings of the 48th International Symposium on Microarchitecture, MICRO-48, 2015.
DOI : 10.1145/2830772.2830775

A. Kennedy, N. Benton, J. B. Jensen, and P. Dagand, Coq, Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming, PPDP '13, pp.13-24
DOI : 10.1145/2505879.2505897
URL : https://hal.archives-ouvertes.fr/hal-01081548

R. Kumar, M. O. Myreen, M. Norrish, and S. Owens, CakeML, Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, pp.179-191
DOI : 10.1145/2535838.2535841

]. X. Leroy, A Formally Verified Compiler Back-end, Journal of Automated Reasoning, vol.27, issue.1
DOI : 10.1007/s10817-009-9155-4
URL : https://hal.archives-ouvertes.fr/inria-00360768

L. Maranget, S. Sarkar, P. Sewell, and P. Mckenney, A tutorial introduction to the ARM and POWER relaxed memory models. Draft available from http Validating memory barriers and atomic instructions, Linux Weekly News article, 2011.

G. Morrisett, G. Tan, J. Tassarotti, J. Tristan, and E. Gan, Rocksalt: better, faster, stronger SFI for the x86, ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '12, pp.395-404, 2012.

D. P. Mulligan, S. Owens, K. E. Gray, T. Ridge, and P. Sewell, Lem: reusable engineering of real-world semantics, Proceedings of ICFP 2014: the 19th ACM SIGPLAN International Conference on Functional Programming, pp.175-188, 2014.

S. Owens, S. Sarkar, and P. Sewell, A Better x86 Memory Model: x86-TSO, Proceedings of TPHOLs 2009: Theorem Proving in Higher Order Logics, pp.391-407, 2009.
DOI : 10.1007/11817963_46

S. Sarkar, P. Sewell, F. Zappa-nardelli, S. Owens, T. Ridge et al., The semantics of x86- CC multiprocessor machine code, Proceedings of POPL 2009: the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, pp.379-391, 2009.

S. Sarkar, P. Sewell, J. Alglave, L. Maranget, and D. Williams, Understanding POWER multiprocessors, Proceedings of PLDI 2011: the 32nd ACM SIGPLAN conference on Programming Language Design and Implementation, pp.175-186, 2011.
DOI : 10.1145/2345156.1993520
URL : https://hal.archives-ouvertes.fr/hal-01100824

P. Sewell, S. Sarkar, S. Owens, F. Z. Nardelli, and M. O. Myreen, x86-TSO, Communications of the ACM, vol.53, issue.7, pp.89-97, 2010.
DOI : 10.1145/1785414.1785443

X. Shi, J. Monin, F. Tuong, and F. Blanqui, First Steps towards the Certification of an ARM Simulator Using Compcert, Certified Programs and Proofs, pp.346-361
DOI : 10.1109/2.982916
URL : https://hal.archives-ouvertes.fr/inria-00624833

J. ?ev?ík, V. Vafeiadis, F. Zappa-nardelli, S. Jagannathan, and P. Sewell, CompCertTSO, Journal of the ACM, vol.60, issue.3, pp.1-22, 2013.
DOI : 10.1145/2487241.2487248