2021
Program Protection Through Software-Based Hardware Abstraction
T. McDonald
,
R. Manikyam
,
S. Bardin
,
R. Bonichon
&
T. Andel
.
SECRYPT.
Search-based Approaches for Local Blackbox Deobfuscation: Understand, Improve and Mitigate
G. Menguy
,
S. Bardin
,
R. Bonichon
&
C. de Souza Lima
.
CCS.
Interface Compliance of Inline Assembly: Automatically Check, Patch and Refine
F. Recoules
,
S. Bardin
,
R. Bonichon
,
M. Lemerre
,
L. Mounier
&
M. Potet
.
ICSE.
Distinguished Paper Award
2020
Binary-level Directed Fuzzing for Use-After-Free Vulnerabilities
M. Nguyen
,
S. Bardin
,
R. Bonichon
,
R. Groz
&
M. Lemerre
.
RAID.
Et TInA RUSTInA le lien vers l'assembleur
F. Recoules
,
S. Bardin
,
R. Bonichon
,
L. Mounier
&
M. Potet
.
JFLA.
2019
How to Kill Symbolic Deobfuscation for Free (or: Unleashing the Potential of Path-Oriented Protections)
M. Ollivier
,
S. Bardin
,
R. Bonichon
&
J. Marion
.
ACSAC.
Obfuscation: Where Are We in Anti-DSE Protections? (a first attempt)
M. Ollivier
,
S. Bardin
,
R. Bonichon
&
J. Marion
.
SSPREW.
Get rid of inline assembly through verification-oriented lifting
F. Recoules
,
S. Bardin
,
R. Bonichon
,
L. Mounier
&
M. Potet
.
ASE.
De l'assembleur sur la ligne ? Appelez TInA !
F. Recoules
,
S. Bardin
,
R. Bonichon
,
L. Mounier
&
M. Potet
.
JFLA.
En finir avec les faux positifs grâce à l’exécution symbolique robuste
B. Farinier
,
S. Bardin
,
R. Bonichon
&
M. Potet
.
JFLA.
2018
Model Generation for Quantified Formulas: A Taint-Based Approach
B. Farinier
,
S. Bardin
,
R. Bonichon
&
M. Potet
.
CAV.
2017
Format unraveled
R. Bonichon
&
P. Weis
.
Journées Francophones des Langages Applicatifs (JFLA).
2015
A syntactic soundness proof for free-variable tableaux with on-the-fly Skolemization
R. Bonichon
&
O. Hermant
.
CoRR.
SMTpp: preprocessors and analyzers for SMT-LIB
R. Bonichon
,
D. Déharbe
,
P. Dobal
&
C. Tavares
.
SMT Workshop.
2014
LLVM-Based Code Generation for B
R. Bonichon
,
D. Déharbe
,
T. Lecomte
&
V. Medeiros Jr.
.
SBMF.
Extending SMT-LIB v2 with \(\lambda\)-Terms and Polymorphism
R. Bonichon
,
D. Déharbe
&
C. Tavares
.
SMT Workshop.
2011
A Mergeable Interval Map
R. Bonichon
&
P. Cuoq
.
Stud. Inform. Univ..
Rigorous Evidence of Freedom from Concurrency Faults in Industrial Control Software
R. Bonichon
,
G. Canet
,
L. Correnson
,
E. Goubault
,
E. Haucourt
,
M. Hirschowitz
,
S. Labbé
&
S. Mimram
.
SAFECOMP.
2007
Zenon : An Extensible Automated Theorem Prover Producing Checkable Proofs
R. Bonichon
,
D. Delahaye
&
D. Doligez
.
LPAR.
2006
On Constructive Cut Admissibility in Deduction Modulo
R. Bonichon
&
O. Hermant
.
TYPES.
A semantic completeness proof for TaMeD
R. Bonichon
&
O. Hermant
.
LPAR.
2004
TaMeD: A Tableau Method for Deduction Modulo
R. Bonichon
.
IJCAR.