Publications


2021

Program Protection Through Software-Based Hardware Abstraction SECRYPT.
Search-based Approaches for Local Blackbox Deobfuscation: Understand, Improve and Mitigate CCS.
Interface Compliance of Inline Assembly: Automatically Check, Patch and Refine ICSE. Distinguished Paper Award

2020

Binary-level Directed Fuzzing for Use-After-Free Vulnerabilities RAID.
Et TInA RUSTInA le lien vers l'assembleur JFLA.

2019

How to Kill Symbolic Deobfuscation for Free (or: Unleashing the Potential of Path-Oriented Protections) ACSAC.
Obfuscation: Where Are We in Anti-DSE Protections? (a first attempt) SSPREW.
Get rid of inline assembly through verification-oriented lifting ASE.
De l'assembleur sur la ligne ? Appelez TInA ! JFLA.
En finir avec les faux positifs grâce à l’exécution symbolique robuste JFLA.

2018

Model Generation for Quantified Formulas: A Taint-Based Approach CAV.

2017

Format unraveled Journées Francophones des Langages Applicatifs (JFLA).

2015

A syntactic soundness proof for free-variable tableaux with on-the-fly Skolemization CoRR.
SMTpp: preprocessors and analyzers for SMT-LIB SMT Workshop.

2014

LLVM-Based Code Generation for B SBMF.
Extending SMT-LIB v2 with \(\lambda\)-Terms and Polymorphism SMT Workshop.

2011

A Mergeable Interval Map Stud. Inform. Univ..
Rigorous Evidence of Freedom from Concurrency Faults in Industrial Control Software SAFECOMP.

2007

Zenon : An Extensible Automated Theorem Prover Producing Checkable Proofs LPAR.

2006

On Constructive Cut Admissibility in Deduction Modulo TYPES.
A semantic completeness proof for TaMeD LPAR.

2004

TaMeD: A Tableau Method for Deduction Modulo IJCAR.