A Precise and Abstract Memory Model for C Using Symbolic Values. - Frédéric Besson; Sandrine Blazy; Pierre Wilke (APLAS, 2014)

A Concrete Memory Model for CompCert. - Frédéric Besson; Sandrine Blazy; Pierre Wilke (ITP, 2015)

Formally verified compilation of low-level C code. (Compilation formellement vérifiée de code C de bas-niveau). - Pierre Wilke (2016)

Compiling Sandboxes: Formally Verified Software Fault Isolation. - Frédéric Besson; Sandrine Blazy; Alexandre Dang; Thomas P. Jensen; Pierre Wilke (ESOP, 2019)

A Verified CompCert Front-End for a Memory Model Supporting Pointer Arithmetic and Uninitialised Data. - Frédéric Besson; Sandrine Blazy; Pierre Wilke (J. Autom. Reason., 2019)

CompCertS: A Memory-Aware Verified C Compiler Using a Pointer as Integer Semantics. - Frédéric Besson; Sandrine Blazy; Pierre Wilke (J. Autom. Reason., 2019)

An abstract stack based approach to verified compositional compilation to machine code. - Yuting Wang 001; Pierre Wilke; Zhong Shao 001 (Proc. ACM Program. Lang., 2019)

Abusing Android Runtime for Application Obfuscation. - Pierre Graux; Jean-François Lalande; Pierre Wilke; Valérie Viet Triem Tong (EuroS&P Workshops, 2020)

Evasive Windows Malware: Impact on Antiviruses and Possible Countermeasures. - Cédric Herzog; Valérie Viet Triem Tong; Pierre Wilke; Arnaud Van Straaten; Jean-Louis Lanet (ICETE (2), 2020)

CompCertELF: verified separate compilation of C programs into ELF object files. - Yuting Wang 001; Xiangzhe Xu; Pierre Wilke; Zhong Shao 001 (Proc. ACM Program. Lang., 2020)

Preventing serialization vulnerabilities through transient field detection. - Pierre Graux; Jean-François Lalande; Valérie Viet Triem Tong; Pierre Wilke (SAC, 2021)

Debiasing Android Malware Datasets: How Can I Trust Your Results If Your Dataset Is Biased? - Tomás Concepción Miranda; Pierre-François Gimenez; Jean-François Lalande; Valérie Viet Triem Tong; Pierre Wilke (IEEE Trans. Inf. Forensics Secur., 2022)

Dada: Debiased Android DAtasets. - Tomás Concepción Miranda; Pierre-François Gimenez; Jean-François Lalande; Valérie Viet Triem Tong; Pierre Wilke (IEEE DataPort, 2022)

A Generic Framework to Develop and Verify Security Mechanisms at the Microarchitectural Level: Application to Control-Flow Integrity. - Matthieu Baty; Pierre Wilke; Guillaume Hiet; Arnaud Fontaine; Alix Trieu (CSF, 2023)

Work in Progress: Thwarting Timing Attacks in Microcontrollers using Fine-grained Hardware Protections. - Nicolas Gaudin; Jean-Loup Hatchikian-Houdot; Frédéric Besson; Pascal Cotret; Guy Gogniat; Guillaume Hiet; Vianney Lapotre; Pierre Wilke (EuroS&P Workshops, 2023)

OATs'inside: Retrieving Object Behaviors From Native-based Obfuscated Android Applications. - Pierre Graux; Jean-François Lalande; Valérie Viet Triem Tong; Pierre Wilke (DTRAP, 2023)

Formal Hardware/Software Models for Cache Locking Enabling Fast and Secure Code. - Jean-Loup Hatchikian-Houdot; Pierre Wilke; Frédéric Besson; Guillaume Hiet (ESORICS (3), 2024)

Side-Channel Resistant Applications through Co-designed Hardware/ Software: the SCRATCHS Project. - Frédéric Besson; Célia Le Du; Pierre Wilke (ERCIM News, 2024)