2024
- A Generic Deskolemization Strategy
J. Rosain, R. Bonichon, J. Cailler, O. Hermant
LPAR 2024, EPiC Series in Computing 100, p. 246–263 · doi
2021
- Program Protection Through Software-Based Hardware Abstraction
T. McDonald, R. Manikyam, S. Bardin, R. Bonichon, T. R. Andel
SECRYPT 2021 · pdf
- Search-based Approaches for Local Blackbox Deobfuscation: Understand, Improve and Mitigate
G. Menguy, S. Bardin, R. Bonichon, C. de Souza Lima
CCS 2021 · pdf
- Interface Compliance of Inline Assembly: Automatically Check, Patch and Refine
F. Recoules, S. Bardin, R. Bonichon, M. Lemerre, L. Mounier, M.-L. Potet
ICSE 2021 — Distinguished Paper Award · pdf
2020
- Binary-level Directed Fuzzing for Use-After-Free Vulnerabilities
M. D. Nguyen, S. Bardin, R. Bonichon, R. Groz, M. Lemerre
RAID 2020 · pdf
- Et TInA RUSTInA le lien vers l'assembleur
F. Recoules, S. Bardin, R. Bonichon, L. Mounier, M.-L. Potet
JFLA 2020 · pdf
2019
- How to Kill Symbolic Deobfuscation for Free (or: Unleashing the Potential of Path-Oriented Protections)
M. Ollivier, S. Bardin, R. Bonichon, J.-Y. Marion
ACSAC 2019 · pdf
- Obfuscation: Where Are We in Anti-DSE Protections? (a first attempt)
M. Ollivier, S. Bardin, R. Bonichon, J.-Y. Marion
SSPREW 2019 · pdf
- Get rid of inline assembly through verification-oriented lifting
F. Recoules, S. Bardin, R. Bonichon, L. Mounier, M.-L. Potet
ASE 2019 · pdf
- De l'assembleur sur la ligne ? Appelez TInA !
F. Recoules, S. Bardin, R. Bonichon, L. Mounier, M.-L. Potet
JFLA 2019 · pdf
- En finir avec les faux positifs grâce à l’exécution symbolique robuste
B. Farinier, S. Bardin, R. Bonichon, M.-L. Potet
JFLA 2019 · pdf
2018
- Model Generation for Quantified Formulas: A Taint-Based Approach
B. Farinier, S. Bardin, R. Bonichon, M.-L. Potet
CAV 2018 · pdf
2017
- Format unraveled
R. Bonichon, P. Weis
JFLA 2017 · pdf · slides
2015
- A syntactic soundness proof for free-variable tableaux with on-the-fly Skolemization
R. Bonichon, O. Hermant
CoRR abs/1505.06376 · arxiv
- SMTpp: preprocessors and analyzers for SMT-LIB
R. Bonichon, D. Déharbe, P. Dobal, C. Tavares
SMT Workshop 2015 · pdf
2014
- LLVM-Based Code Generation for B
R. Bonichon, D. Déharbe, T. Lecomte, V. Medeiros Jr
SBMF 2014
- Extending SMT-LIB v2 with \(\lambda\)-Terms and Polymorphism
R. Bonichon, D. Déharbe, C. Tavares
SMT Workshop 2014 · pdf
2011
- A Mergeable Interval Map
R. Bonichon, P. Cuoq
Stud. Inform. Univ. 9(1), p. 5–37 · pdf
- 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 2011, p. 85–98 · pdf · doi
2007
- Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
R. Bonichon, D. Delahaye, D. Doligez
LPAR 2007 · pdf
2006
- On Constructive Cut Admissibility in Deduction Modulo
R. Bonichon, O. Hermant
TYPES 2006 · pdf
- A semantic completeness proof for TaMeD
R. Bonichon, O. Hermant
LPAR 2006 · pdf
2004
- TaMeD: A Tableau Method for Deduction Modulo
R. Bonichon
IJCAR 2004, p. 445–459 · pdf · doi