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