J. Abrial, M. Butler, S. Hallerstede, T. S. Hoang, F. Mehta et al., Rodin: an open toolset for modelling and reasoning in Event-B, International Journal on Software Tools for Technology Transfer, vol.15, issue.1, 2010.
DOI : 10.1007/978-3-642-18216-7

A. Development and T. , The Agda theorem prover, version 2.5.3

O. Agesen, D. Detlefs, A. Garthwaite, R. Knippel, Y. S. Ramakrishna et al., An Efficient Meta-lock for Implementing Ubiquitous Synchronization, 1999.
DOI : 10.1145/320384.320402
URL : http://cs.unomaha.edu/~stanw/papers/csci8550/p207-agesen.pdf

J. Alglave, A formal hierarchy of weak memory models, Formal Methods in System Design, vol.19, issue.3, pp.178-210, 2012.
DOI : 10.1145/115953.115964

J. Alglave, D. Kroening, and M. Tautschnig, Partial Orders for Efficient Bounded Model Checking of??Concurrent??Software, International Conference on Computer Aided Verification. Proc. of CAV'13, 2013.
DOI : 10.1007/978-3-642-39799-8_9

J. Alglave, L. Maranget, and M. Tautschnig, Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory, In: TOPLAS' ACM Transactions on Programming Languages and Systems, vol.14, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01081413

S. Amani, J. Andronick, M. Bortin, C. Lewis, C. Rizkallah et al., Complx: a verification framework for concurrent imperative programs, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, 2017.
DOI : 10.1016/j.tcs.2006.12.035

A. Anand, A. Appel, G. Morrisett, Z. Paraskevopoulou, R. Pollack et al., CertiCoq: A verified compiler for Coq

. Coqpl, 17: International Workshop on Coq for Programming Languages, 2017.

A. W. Appel, R. Dockins, A. Hobor, L. Beringer, J. Dodds et al., Program Logics for Certified Compilers, 2014.
DOI : 10.1017/CBO9781107256552

E. A. Ashcroft and Z. Manna, Formalization of properties of parallel programs, In: Machine Intelligence, vol.6, 1971.

T. Balabonski, F. Pottier, J. Protzenko, and N. Williams, Type Soundness and Race Freedom for Mezzo, Proc. of FLOPS Dependable Systems and Networks, 2002.
DOI : 10.1007/978-3-319-07151-0_16
URL : https://hal.archives-ouvertes.fr/hal-01081194

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development: Coq'Art The Calculus of Inductive Constructions . 1st, 2010.
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/hal-00344237

B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne et al., A Static Analyzer for Large Safety-Critical Software In: Programming Language Design and Implementation, Proc. of PLDI'03, 2003.

S. Brookes, A Semantics for Concurrent Separation Logic, In: Theoretical Computer Science, vol.375, pp.1-3, 2007.
DOI : 10.1016/j.tcs.2006.12.034
URL : https://doi.org/10.1016/j.tcs.2006.12.034

C. J. Cheney, A nonrecursive list compacting algorithm, Communications of the ACM, vol.13, issue.11, pp.677-678, 1970.
DOI : 10.1145/362790.362798

A. Chlipala, A Verified Compiler for an Impure Functional Language, Symposium on Principles of Programming Languages. Proc. of POPL'10, 2010.
DOI : 10.1145/1706299.1706312
URL : http://www.cs.berkeley.edu/~adamc/tmp/imp.pdf

A. Chlipala, Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant, 2013.

J. W. Coleman and C. B. Jones, A Structural Proof of the Soundness of Rely/guarantee Rules, Journal of Logic and Computation, vol.17, issue.4, pp.807-841, 2007.
DOI : 10.1093/logcom/exm030

. Collective, Static Single Assignment Book, 2015.

G. E. Collins, A method for overlapping and erasure of lists, Communications of the ACM, vol.3, issue.12, pp.655-657, 1960.
DOI : 10.1145/367487.367501

C. Development and T. , The CompCert verified compiler, version 3.0

C. Development and T. , The Coq Reference Manual, version 8.4 Available at https

R. Cytron, J. Ferrante, B. K. Rosen, M. N. Wegman, and F. K. Zadeck, Efficiently computing static single assignment form and the control dependence graph, ACM Transactions on Programming Languages and Systems, vol.13, issue.4, pp.451-490, 1991.
DOI : 10.1145/115372.115320
URL : http://grothoff.org/christian/teaching/2007/3353/papers/ssa.pdf

J. Davis and M. O. Myreen, The Reflective Milawa Theorem Prover is Sound (Down to the Machine Code that Runs it), Journal of Automated Reasoning, vol.411, issue.50, pp.117-183, 2015.
DOI : 10.1016/j.tcs.2010.09.014

L. De, M. , and N. Bjørner, Z3: An Efficient SMT Solver In: Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS'08/ETAPS'08, 2008.

D. Demange, Semantic foundations of intermediate program representations Theses. École normale supérieure de Cachan -ENS Cachan

J. Derrick, G. Schellhorn, and H. Wehrheim, Mechanically verified proof obligations for linearizability, ACM Transactions on Programming Languages and Systems, vol.33, issue.1, 2011.
DOI : 10.1145/1889997.1890001

E. W. Dijkstra, L. Lamport, A. J. Martin, C. S. Scholten, and E. F. Steffens, On-the-fly garbage collection: an exercise in cooperation, Communications of the ACM, vol.21, issue.11, pp.11-966, 1978.
DOI : 10.1145/359642.359655

T. Dinsdale-young, M. Dodds, P. Gardner, M. J. Parkinson, and V. Vafeiadis, Concurrent Abstract Predicates, European Conference on Object-oriented Programming. Proc. of ECOOP'10, 2010.
DOI : 10.1007/978-3-642-14107-2_24
URL : http://www.doc.ic.ac.uk/%7Epg/papers/cap.pdf

M. Doko and V. Vafeiadis, A Program Logic for C11 Memory Fences, Proceedings of the 10th International Conference on Verification, Model Checking, and Abstract Interpretation. VMCAI'09, 2016.
DOI : 10.1007/978-3-662-49122-5_20

D. Doligez and G. Gonthier, Portable, unobtrusive garbage collection for multiprocessor systems, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '94, 1994.
DOI : 10.1145/174675.174673

D. Doligez and X. Leroy, A concurrent, generational garbage collector for a multithreaded implementation of ML, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '93, 1993.
DOI : 10.1145/158511.158611
URL : https://hal.archives-ouvertes.fr/hal-01499969

D. Doligez, Conception, réalisation et certification d'un glaneur de cellules concurrent, 1995.

T. Domani, E. K. Kolodner, E. Lewis, E. E. Salant, K. Barabash et al., Implementing an On-the-Fly Garbage Collector for Java, Symposium on Memory management. Proc. of ISMM'00, 2000.

B. Dongol and J. Derrick, Verifying Linearisability, ACM Computing Surveys, vol.48, issue.2, 2015.
DOI : 10.1007/978-3-642-29952-0_12
URL : http://bura.brunel.ac.uk/bitstream/2438/11530/1/Fulltext.pdf

M. Dowson, The Ariane 5 software failure, ACM SIGSOFT Software Engineering Notes, vol.22, issue.2, p.84, 1997.
DOI : 10.1145/251880.251992

E. Eide and J. Regehr, Volatiles are miscompiled, and what to do about it, Proceedings of the 7th ACM international conference on Embedded software, EMSOFT '08, 2008.
DOI : 10.1145/1450058.1450093
URL : http://www.cs.utah.edu/~regehr/papers/emsoft08-preprint.pdf

. Facebook, Infer: a static program analyser for Java, C and Objective- C. http://fbinfer

X. Feng, Local Rely-guarantee Reasoning, Symposium on Principles of Programming Languages. Proc. of POPL'09, 2009.
DOI : 10.1145/1594834.1480922
URL : http://flint.cs.yale.edu/cs428/doc/lrg-tr.pdf

X. Feng, R. Ferreira, and Z. Shao, On the Relationship Between Concurrent Separation Logic and Assumeguarantee Reasoning, European Conference on Programming. ESOP'07, 2007.

R. Robert, J. C. Fenichel, and . Yochelson, A LISP Garbagecollector for Virtual-memory Computer Systems, In: Communication of the ACM, vol.12, issue.11, pp.611-612, 1969.

I. Filipovi´cfilipovi´c, O. Peter, N. Hearn, H. Rinetzky, and . Yang, Abstraction for Concurrent Objects, European Symposium on Programming Languages and Systems. ESOP '09, 2009.

S. Flur, K. E. Gray, C. Pulte, S. Sarkar, A. Sezgin et al., Modelling the ARMv8 architecture, operationally: concurrency and ISA, Symposium on Principles of Programming Languages. Proc. of POPL'16, 2016.
DOI : 10.1145/2914770.2837615
URL : https://hal.archives-ouvertes.fr/hal-01244776

P. Gammie, A. L. Hosking, and K. Engelhardt, Relaxing safely: verified on-the-fly garbage collection for x86-TSO, Programming Language Design and Implementation. Proc. of PLDI 2015, 2015.

G. Gonthier, Verifying the safety of a practical concurrent garbage collector, International Conference on Computer Aided Verification. Proc. of CAV'96, 1996.
DOI : 10.1007/3-540-61474-5_103

G. Gonthier, The Four Colour Theorem: Engineering of a Formal Proof, 8th Asian Symposium . ASCM'07, 2007.
DOI : 10.1007/978-3-540-87827-8_28

H. Development and T. , The HOL4 theorem prover, version Kananaskis-11 Available at https://hol-theorem-prover.org, 2017.

D. Halperin, T. S. Heydt-benjamin, B. Ransford, S. S. Clark, B. Defend et al., Pacemakers and Implantable Cardiac Defibrillators: Software Radio Attacks and Zero-Power Defenses, 2008 IEEE Symposium on Security and Privacy (sp 2008), 2008.
DOI : 10.1109/SP.2008.31
URL : http://scholarworks.umass.edu/cgi/viewcontent.cgi?article=1067&context=cs_faculty_pubs

. Per-brinch-hansen, Monitors and Concurrent Pascal: A Personal History, In: ACM SIGPLAN Conference on History of Programming Languages. HOPL-II, 1993.

T. L. Harris, K. Fraser, and I. A. Pratt, A Practical Multi-word Compare-and-Swap Operation, International Conference on Distributed Computing. Proc. of DISC'02, 2002.
DOI : 10.1007/3-540-36108-1_18
URL : http://www.cl.cam.ac.uk/Research/SRG/netos/papers/2002-casn.ps

K. Havelund, Mechanical verification of a garbage collector, International Parallel Processing Symposium and Symposium on Parallel and Distributed Processing. Proc. of IPPS/SPDP'99, 1999.
DOI : 10.1007/BFb0098007

C. Hawblitzel and E. Petrank, Automated verification of practical garbage collectors, Symposium on Principles of Programming Languages Proc of POPL'09, 2009.
DOI : 10.2168/lmcs-6(3:6)2010
URL : http://arxiv.org/pdf/1004.3808

C. Hawblitzel, J. Howell, J. R. Lorch, A. Narayan, B. Parno et al., Ironclad Apps: End-to-end Security via Automated Full-system Verification, USENIX Conference on Operating Systems Design and Implementation . Proc. of OSDI'14, 2014.

D. Hendler, N. Shavit, and L. Yerushalmi, A Scalable Lock-free Stack Algorithm, ACM Symposium on Parallelism in Algorithms and Architectures. Proc. of SPAA '04, 2004.
DOI : 10.1145/1007912.1007944
URL : http://www.cs.bgu.ac.il/~hendlerd/papers/scalable-stack.pdf

M. Herlihy and J. M. Wing, Linearizability: a correctness condition for concurrent objects, ACM Transactions on Programming Languages and Systems, vol.12, issue.3, pp.463-492, 1990.
DOI : 10.1145/78969.78972
URL : http://www.cs.uoregon.edu/classes/06W/cis607atom/readings/herlihy-linearizability.pdf

M. Herlihy and N. Shavit, The art of multiprocessor programming, Proceedings of the twenty-fifth annual ACM symposium on Principles of distributed computing , PODC '06, 2008.
DOI : 10.1145/1146381.1146382

T. Hoare, An Axiomatic Basis for Computer Programming, In: Communications of the ACM, vol.1210, pp.576-580, 1969.
DOI : 10.1007/978-94-011-1793-7_5
URL : http://www.utdallas.edu/~kxh060100/cs6371fa07/hoare.pdf

T. Hoare, Monitors: An Operating System Structuring Concept In: The Origin of Concurrent Programming: From Semaphores to Remote Procedure Calls, pp.272-294, 2002.

M. Hofmann and M. Pavlova, Elimination of Ghost Variables in Program Logics, Conference on Trustworthy Global Computing. Proc. of TGC'07, 2008.
DOI : 10.1007/978-3-540-78663-4_1

I. Development and T. , The Isabelle theorem prover, version 2016-1

S. Samin, P. W. Ishtiaq, and . Hearn, BI As an Assertion Language for Mutable Data Structures, p.1, 2001.

]. S. Jagannathan, V. Laporte, G. Petri, D. Pichardie, and J. Vitek, Atomicity Refinement for Verified Compilation, ACM Transactions on Programming Languages and Systems, vol.14, issue.6, pp.1-630, 2014.
DOI : 10.1145/2666356.2594346
URL : https://hal.archives-ouvertes.fr/hal-01102435

C. B. Jones, Tentative steps toward a development method for interfering programs, ACM Transactions on Programming Languages and Systems, vol.5, issue.4, pp.596-619, 1983.
DOI : 10.1145/69575.69577
URL : http://staff.ustc.edu.cn/~xyfeng/reading/p596-jones-RG.pdf

R. Jones, A. Hosking, and E. Moss, The Garbage Collection Handbook: The Art of Automatic Memory Management, 2011.
DOI : 10.1201/9781315388021

R. Jones and R. Lins, Garbage Collection: Algorithms for Automatic Dynamic Memory Management, 1996.

H. B. Jonkers, A fast garbage compaction algorithm, Information Processing Letters, vol.9, issue.1, 1979.
DOI : 10.1016/0020-0190(79)90103-0

R. Jung, D. Swasey, F. Sieczkowski, K. Svendsen, A. Turon et al., Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning, Symposium on Principles of Programming Languages. Proc. of POPL'15, 2015.

R. Jung, J. Jourdan, R. Krebbers, and D. Dreyer, RustBelt: securing the foundations of the rust programming language, Symposium on Principles of Programming Languages. Proc. of POPL'18, 2018.
DOI : 10.1145/2500365.2500600
URL : https://hal.archives-ouvertes.fr/hal-01633165

J. Kaiser, H. Dang, D. Dreyer, O. Lahav, and V. Vafeiadis, Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris, European Conference on Object-Oriented Programming. Proc. of ECOOP'17, 2017.

D. Kästner, X. Leroy, S. Blazy, B. Schommer, M. Schmidt et al., Closing the gap ? The formally verified optimizing compiler CompCert, Safety-critical Systems Symposium . Proc. of SSS'17, 2017.

R. Krebbers, A. Timany, and L. Birkedal, Interactive Proofs in Higher-order Concurrent Separation Logic, Symposium on Principles of Programming Languages. Proc. of POPL'17, 2017.
DOI : 10.1145/3093333.3009855
URL : https://lirias.kuleuven.be/bitstream/123456789/553559/1/paper.pdf

R. Krebbers, R. Jung, A. Bizjak, J. Jourdan, D. Dreyer et al., The Essence of Higher-Order Concurrent Separation Logic, European Symposium on Programming Languages and Systems. ESOP'17, 2017.
DOI : 10.1145/2500365.2500600
URL : https://hal.archives-ouvertes.fr/hal-01633133

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, 2014.
DOI : 10.1145/2535838.2535841

H. T. Kung and S. W. Song, An efficient parallel garbage collection system and ITS correctness proof, 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), 1977.
DOI : 10.1109/SFCS.1977.5
URL : http://www.dtic.mil/cgi-bin/GetTRDoc?AD=ADA046626&Location=U2&doc=GetTRDoc.pdf

O. Lahav and V. Vafeiadis, Owicki-Gries Reasoning for Weak Memory Models, International Colloquium on Automata, Languages, and Programming. Proc. of ICALP'15, 2015.
DOI : 10.1007/978-3-662-47666-6_25

L. Lamport, How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs, IEEE Transactions on Computers, vol.28, issue.9, pp.690-691, 1979.
DOI : 10.1109/TC.1979.1675439

C. Arthur and L. , LLVM: An infrastructure for multi-stage optimization, 2002.

L. Development and T. , The Lean theorem prover, version 3.3.0. Available at https://leanprover.github.io, 2017.

D. Leinenbach, W. J. Paul, and E. Petrova, Towards the formal verification of a C0 compiler: code generation and implementation correctness, Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), 2005.
DOI : 10.1109/SEFM.2005.51

K. Rustan and M. Leino, This is Boogie 2, 2008.

X. Leroy, A Formally Verified Compiler Back-end, Journal of Automated Reasoning, vol.27, issue.1, 2009.
DOI : 10.1007/978-3-642-59495-3
URL : https://hal.archives-ouvertes.fr/inria-00360768

H. Liang and X. Feng, Modular verification of linearizability with non-fixed linearization points In: Programming Language Design and Implementation, Proc. of PLDI'03, 2013.

H. Liang, X. Feng, and M. Fu, A Rely-Guarantee-based simulation for verifying concurrent program transformations, Symposium on Principles of Programming Languages. Proc. of POPL'12, 2012.

H. Liang, X. Feng, and M. Fu, Rely-Guarantee-Based Simulation for Compositional Verification of Concurrent Program Transformations, ACM Transactions on Programming Languages and Systems, vol.36, issue.1, pp.1-355, 2014.
DOI : 10.1016/j.tcs.2006.12.036

H. Liang, X. Feng, and Z. Shao, Compositional verification of termination-preserving refinement of concurrent programs, Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, 2014.
DOI : 10.1145/2603088.2603123

H. Liang, J. Hoffmann, X. Feng, and Z. Shao, Characterizing Progress Properties of Concurrent Objects via Contextual Refinements, International Conference on Concurrency Theory. CONCUR'13, 2013.
DOI : 10.1007/978-3-642-40184-8_17

H. Lieberman and C. Hewitt, A real-time garbage collector based on the lifetimes of objects, Communications of the ACM, vol.26, issue.6, pp.419-429, 1983.
DOI : 10.1145/358141.358147

W. Mansky, Y. Peng, S. Zdancewic, and J. Devietti, Verifying dynamic race detection, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, 2017.
DOI : 10.1145/1791194.1791203

J. Mccarthy, Recursive functions symbolic expressions and their computation by machine, Part I, Communications of the ACM, vol.3, issue.4, pp.184-195, 1960.
DOI : 10.1145/367177.367199

A. Mccreight, T. Chevalier, and A. Tolmach, A Certified Framework for Compiling and Executing Garbagecollected Languages, International Conference on Functional Programming. Proc. of ICFP '10, 2010.

A. Mccreight, Z. Shao, C. Lin, and L. Li, A General Framework for Certifying Garbage Collectors and Their Mutators In: Programming Language Design and Implementation, Proc. of PLDI'07, 2007.

J. Mccarthy and J. Painter, Correctness of a compiler for arithmetic expressions, 1967.
DOI : 10.1090/psapm/019/0242403

M. Maged, M. L. Michael, and . Scott, Simple, Fast, and Practical Non-blocking and Blocking Concurrent Queue Algorithms, ACM Symposium on Principles of Distributed Computing . Proc. of PODC '96, 1996.

M. Development and T. , The Mizar System, version 8.1.05 Available at http://mizar.org/system, 2016.

J. Moore, A mechanically verified language implementation, Journal of Automated Reasoning, vol.5, issue.4, pp.461-492, 1989.
DOI : 10.1007/BF00243133
URL : http://www.cs.utexas.edu/users/boyer/ftp/cli-reports/030.pdf

S. Moore, Piton: A Mechanically Verified Assembly-level Language, 1996.
DOI : 10.1007/bf00243133
URL : http://www.cs.utexas.edu/users/boyer/ftp/cli-reports/030.pdf

F. and L. Morris, Advice on structuring compilers and proving them correct, Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '73, 1973.
DOI : 10.1145/512927.512941

M. O. Myreen, Reusable Verification of a Copying??Collector, Conference on Verified Software: Theories, Tools, Experiments. VSTTE'10, 2010.
DOI : 10.1007/978-3-642-15057-9_10

A. Nanevski, R. Ley-wild, I. Sergey, and G. Delbianco, Communicating State Transition Systems for Fine-Grained Concurrent Resources, European Symposium on Programming. Proc. of ESOP'14, 2014.
DOI : 10.1007/978-3-642-54833-8_16
URL : http://software.imdea.org/~aleks/papers/concur/esop14.pdf

C. Newcombe, T. Rath, F. Zhang, B. Munteanu, M. Brooker et al., How Amazon web services uses formal methods, Communications of the ACM, vol.58, issue.4, pp.66-73, 2015.
DOI : 10.1145/2185376.2185383

K. Nienhuis, K. Memarian, and P. Sewell, An operational semantics for C/C++11 concurrency, International Conference on Object-Oriented Programming, Systems, Languages , and Applications. Proc. of OOPSLA'16, 2016.
DOI : 10.1145/2983990.2983997

L. Nieto, The Rely-Guarantee Method in Isabelle/HOL, European Conference on Programming. Proc. of ESOP'03, 2003.
DOI : 10.1007/3-540-36575-3_24

T. Nipkow and L. P. Nieto, Owicki/Gries in Isabelle/HOL, Proc. of FASE'99, 1999.
DOI : 10.1007/978-3-540-49020-3_13
URL : https://link.springer.com/content/pdf/10.1007%2F978-3-540-49020-3_13.pdf

P. W. O-'hearn, Separation logic and concurrent resource management, International Symposium on Memory Management. Proc. of ISMM'07, 2007.

S. Owens, Reasoning about the Implementation of Concurrency Abstractions on x86-TSO, European Conference on Object-oriented Programming. Proc. of ECOOP'10, 2010.
DOI : 10.1007/978-3-642-14107-2_23

S. Owens, S. Sarkar, and P. Sewell, A Better x86 Memory Model: x86-TSO, Theorem Proving in Higher Order Logics, 22nd International Conference, pp.391-407, 2009.
DOI : 10.1109/IPDPS.2004.1302944
URL : http://www.cl.cam.ac.uk/~ss726/papers/x86tso09.pdf

S. S. Owicki, Axiomatic Proof Techniques for Parallel Programs. Outstanding Dissertations in the Computer Sciences, 1975.
DOI : 10.1007/978-1-4612-6315-9_12

S. Owicki and D. Gries, Verifying properties of parallel programs: an axiomatic approach, Communications of the ACM, vol.19, issue.5, pp.279-285, 1976.
DOI : 10.1145/360051.360224

T. Pvs-development, The PVS Specification and Verification System, version 6.0

M. Paleczny, C. Vick, and C. Click, The Java hotspotTM Server Compiler, Symposium on JavaTM Virtual Machine Research and Technology. JVM'01, 2001.

M. Parkinson, The Next 700 Separation Logics, 2010.
DOI : 10.1007/978-3-642-15057-9_12

D. Pavlovic, P. Pepper, and D. R. Smith, Formal Derivation of Concurrent Garbage Collectors, Mathematics of Program Construction. MPC'10, 2010.
DOI : 10.1007/978-3-642-13321-3_20

L. P. Simon, A. L. Jones, and . Santos, A Transformationbased Optimiser for Haskell, In: Science of Computer Programming, vol.32, pp.1-3, 1998.

S. Peyton, J. , and S. Marlow, Secrets of the Glasgow Haskell Compiler inliner, Journal of Functional Programming, vol.12, issue.4-5, pp.393-434, 2002.
DOI : 10.1017/S0956796802004331

F. Pfenning and C. Elliott, Higher-Order Abstract Syntax In: Programming Language Design and Implementation, Proc. of PLDI'88, 1988.

C. Benjamin, A. Pierce, C. Azevedo-de-amorim, M. Casinghino, M. Gaboardi et al., Software Foundations. Version 5.0, 2017.

F. Pizlo and J. Vitek, Memory Management for Real-Time Java: State of the Art, 2008 11th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing (ISORC), 2008.
DOI : 10.1109/ISORC.2008.40

L. Nieto, The Rely-Guarantee Method in Isabelle/HOL, European Symposium on Programming. ESOP'03, 2003.
DOI : 10.1007/3-540-36575-3_24

J. C. Reynolds, Separation logic: a logic for shared mutable data structures, Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, 2002.
DOI : 10.1109/LICS.2002.1029817
URL : http://ttic.uchicago.edu/~dreyer/seplogic.pdf

T. Ridge, A Rely-Guarantee Proof System for x86-TSO, International Conference on Verified Software: Theories, Tools, Experiments . VSTTE'10, 2010.
DOI : 10.1007/978-3-642-15057-9_4
URL : http://www.cs.le.ac.uk/people/tr61/doc/ridge10vstte.pdf

M. Samek, Are we shooting ourselves in the foot with Stack Overflow? http : / / embeddedgurus . com / state -space / 2014 / 02 / are -we -shooting -ourselves -in -the -foot -with -stack overflow, 2014.

A. Sandberg-ericsson, M. O. Myreen, and J. Å. Pohjola, A Verified Generational Garbage Collector for CakeML, Interactive Theorem Proving. Proc. of ITP'17, 2017.
DOI : 10.1145/1806596.1806610

S. Sarkar, P. Sewell, J. Alglave, L. Maranget, and D. Williams, Understanding POWER Multiprocessors In: Programming Language Design and Implementation, Proc. of PLDI'11

R. A. Saunders, The LISP system for the Q-32 computer In: The programming language LISP: its operation and applications, pp.220-231, 1974.

I. Sergey, A. Nanevski, and A. Banerjee, Mechanized verification of fine-grained concurrent programs In: Programming Language Design and Implementation, Proc. of PLDI'15, 2015.

I. Sergey, A. Nanevski, and A. Banerjee, Mechanized Verification of Fine-grained Concurrent Programs In: Programming Language Design and Implementation, Proc. of PLDI'15, 2015.

J. ?ev?ík, V. Vafeiadis, F. Z. Nardelli, S. Jagannathan, and P. Sewell, CompCertTSO, Journal of the ACM, vol.60, issue.3, p.22, 2013.
DOI : 10.1145/2487241.2487248

F. Sieczkowski, K. Svendsen, L. Birkedal, and J. Pichon-pharabod, A Separation Logic for Fictional Sequential Consistency, European Symposium on Programming. ESOP'15, 2015.
DOI : 10.1007/978-3-662-46669-8_30

Y. Kiam-tan, M. O. Myreen, R. Kumar, A. Fox, S. Owens et al., A New Verified Compiler Backend for CakeML, Proc. of ICFP'16, 2016.

N. Torp-smith, L. Birkedal, and J. C. Reynolds, Local reasoning about a copying garbage collector, ACM Transactions on Programming Languages and Systems, vol.30, issue.4, pp.1-2458, 2008.
DOI : 10.1145/1377492.1377499
URL : http://www.itu.dk/people/noah/papers/gc-popl.ps

R. K. Treiber, Systems Programming: Coping with Parallelism, 1986.

D. Ungar, Generation Scavenging: A Non-Disruptive High Performance Storage Reclamation Algorithm, 1984.

V. Vafeiadis, Modular Fine-Grained Concurrency Verification, 2007.

V. Vafeiadis and M. J. Parkinson, A Marriage of Rely/Guarantee and Separation Logic, International Conference on Concurrency Theory. CONCUR'07, 2007.
DOI : 10.1007/978-3-540-74407-8_18

V. Vafeiadis, Automatically Proving Linearizability, International Conference on Computer Aided Verification. Proc. of CAV'10, 2010.
DOI : 10.1007/978-3-642-14295-6_40
URL : http://www.cl.cam.ac.uk/%7Evv216/papers/cav2010-linear.pdf

V. Vafeiadis and C. Narayan, Relaxed Separation Logic: A Program Logic for C11 Concurrency, International Conference on Object Oriented Programming Systems Languages and Applications. Proc. of OOPSLA'13, 2013.
DOI : 10.1145/2509136.2509532

M. Wildmoser and T. Nipkow, Certifying Machine Code Safety: Shallow Versus Deep Embedding, Theorem Proving in Higher Order Logics. TPHOLs'04, 2004.
DOI : 10.1007/978-3-540-30142-4_22
URL : http://www.in.tum.de/~nipkow/pubs/tphols04.pdf

R. Paul and . Wilson, Uniprocessor Garbage Collection Techniques In: International Workshop on Memory Management, Proc. of IWMM'92, 1992.

G. Winskel, The Formal Semantics of Programming Languages: An Introduction, 1993.

A. Witze, Software error doomed Japanese Hitomi spacecraft, Nature, vol.533, issue.7601, pp.18-19, 2016.
DOI : 10.1038/nature.2016.19835

A. K. Wright and M. Felleisen, A Syntactic Approach to Type Soundness, Information and Computation, vol.115, issue.1, pp.38-94, 1994.
DOI : 10.1006/inco.1994.1093
URL : https://doi.org/10.1006/inco.1994.1093

J. Yang and C. Hawblitzel, Safe to the Last Instruction: Automated Verification of a Type-safe Operating System In: Programming Language Design and Implementation, Proc. of PLDI'10, 2010.

X. Yang, Y. Chen, E. Eide, and J. Regehr, Finding and Understanding Bugs in C Compilers, Proc. of PLDI'11, 2011.
DOI : 10.1145/1993316.1993532
URL : http://www.stanford.edu/class/cs343/resources/finding-bugs-compilers.pdf

Y. Zakowski, D. Cachera, D. Demange, G. Petri, D. Pichardie et al., Verifying a Concurrent Garbage Collector Using a Rely-Guarantee Methodology, Interactive Theorem Proving. Proc. of ITP'17, 2017.
DOI : 10.1007/978-3-540-74407-8_18
URL : https://hal.archives-ouvertes.fr/hal-01613389

Y. Zakowski, D. Cachera, D. Demange, and D. Pichardie, Compilation of Linearizable Data Structures -A Mechanised RG Logic for Semantic Refinement, Symposium on Applied Computing. Proc. of SAC'18, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01538128

J. Zhao, S. Nagarakatte, M. Milo, S. Martin, and . Zdancewic, Formalizing the LLVM Intermediate Representation for Verified Program Transformations, In: Symposium on
DOI : 10.1145/2103656.2103709
URL : https://repository.upenn.edu/cgi/viewcontent.cgi?article=1743&context=cis_papers