Secure Compilation of Constant-Resource Programs, with Gilles Barthe, Rémi Hutin and David Pichardie,
CSF 2021
Formally Verified Speculation and Deoptimization in a JIT Compiler, with Aurèle Barrière, Olivier Flückiger, David Pichardie and Jan Vitek.
POPL 2021
A Fast Verified Liveness Analysis in SSA Form, with Jean-Christophe Léchenet and David Pichardie.
IJCAR 2020
Formal Verification of a Constant-Time Preserving C Compiler, with Gilles Barthe, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie and Alix Trieu.
POPL 2020
Teaching Deductive Verification in Why3 to Undergraduate Students.
FMTea 2019
Compiling Sandboxes: Formally Verified Software Fault Isolation, with Frédéric Besson, Alexandre Dang, Thomas Jensen and Pierre Wilke.
ESOP 2019
Formal verification of a program obfuscation based on mixed boolean-arithmetic expressions, with
Rémi Hutin.
CPP 2019
L'assistant de preuve Coq, with Pierre Castéran and Hugo Herbelin.
Techniques de l'Ingénieur, 2017
Verified Constant-Time Implementations by Abstract Interpretation, with David Pichardie and Alix Trieu.
ESORICS 2017
CompCertS: a memory-aware verified C compiler using pointer as integer semantics, with
Frédéric Besson and Pierre Wilke.
ITP 2017
Verified Translation Validation of Static Analyses, with Gilles Barthe, Vincent Laporte, David Pichardie and Alix Trieu.
CSF 2017
Structuring Abstract Interpreters Through State and Value Abstractions, with David Bühler and Boris Yakobowski.
VMCAI 2017
An Abstract Memory Functor for Verified C Static Analyzers, with Vincent Laporte and David Pichardie.
ICFP 2016
CompCert - A formally verified optimizing compiler,
with Xavier Leroy, Daniel Kästner, Bernhard
Schommer, Markus Pister and Christian Ferdinand.
ERTS2 2016
Formal verification of control flow flattening, with
Alix Trieu.
CPP 2016
Data tainting and Obfuscation: Improving Plausibility of Incorrect Taint, with
Stéphanie Riaud and Thomas Sirvent.
SCAM 2015
Validating Dominator Trees for a Fast, Verified Dominance Test, with
Delphine Demange and David Pichardie.
ITP 2015
A concrete memory model for CompCert, with
Frédéric Besson and Pierre Wilke.
ITP 2015
A formally-verified C static analyzer, with Jacques-Henri Jourdan,
Vincent Laporte, Xavier Leroy and David Pichardie.
POPL 2015
Verified validation of program slicing, with
André Maroneze and David Pichardie.
CPP 2015
A Precise and Abstract Memory Model for C using
Symbolic Values, with Frédéric
Besson and Pierre Wilke.
APLAS 2014
Improving Static Analyses of C Programs with Conditional Predicates, with
David Bühler and Boris Yakobowski.
FMICS 2014. Best paper award.
Verified Abstract Interpretation Techniques for
Disassembling Low-level Self-modifying Code, with
Vincent Laporte and David Pichardie.
ITP 2014.
A Formally Verified WCET Estimation Tool, with
André Maroneze, David Pichardie and Isabelle
Puaut.
WCET 2014
The CompCert memory model, with Xavier Leroy, Andrew Appel, Gordon
Stewart.
In
Program Logics for Certified Compilers. Cambridge University Press. 2014.
Proofs
you can believe in - Proving equivalences between Prolog
semantics in Coq, with
Jael Kriener and Andy King.
PPDP 2013 .
Formal
Verification
of Loop Bound Estimation for WCET Analysis, with
Andre Maroneze and David Pichardie.
VSTTE 2013 .
Formal
Verification of a C Value Analysis Based on Abstract
Interpretation, with Vincent Laporte, Andre
Maroneze and David Pichardie.
SAS 2013 .