Exploring Robust Property Preservation for Secure Compilation. - Carmine Abate; Roberto Blanco; Deepak Garg 001; Catalin Hritcu; Marco Patrignani; Jérémy Thibault (CoRR, 2018)

Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation. - Carmine Abate; Roberto Blanco; Deepak Garg 001; Catalin Hritcu; Marco Patrignani; Jérémy Thibault (CSF, 2019)

Trace-Relating Compiler Correctness and Secure Compilation. - Carmine Abate; Roberto Blanco; Stefan Ciobaca; Deepak Garg 001; Catalin Hritcu; Marco Patrignani; Éric Tanter; Jérémy Thibault (CoRR, 2019)

Trace-Relating Compiler Correctness and Secure Compilation. - Carmine Abate; Roberto Blanco; Stefan Ciobaca; Adrien Durier; Deepak Garg 001; Catalin Hritcu; Marco Patrignani; Éric Tanter; Jérémy Thibault (ESOP, 2020)

An Extended Account of Trace-relating Compiler Correctness and Secure Compilation. - Carmine Abate; Roberto Blanco; Stefan Ciobaca; Adrien Durier; Deepak Garg 001; Catalin Hritcu; Marco Patrignani; Éric Tanter; Jérémy Thibault (ACM Trans. Program. Lang. Syst., 2021)

SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking Simulation. - Akram El-Korashy; Roberto Blanco; Jérémy Thibault; Adrien Durier; Deepak Garg 001; Catalin Hritcu (CSF, 2022)

SECOMP: Formally Secure Compilation of Compartmentalized C Programs. - Jérémy Thibault; Roberto Blanco; Dongjae Lee; Sven Argo; Arthur Azevedo de Amorim; Aïna Linn Georges; Catalin Hritcu; Andrew Tolmach (CCS, 2024)

Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs. - Jérémy Thibault; Joseph Lenormand; Catalin Hritcu (CoRR, 2025)