| 2024 | LPAR | A Generic Deskolemization Strategy. | Johann Rosain, Richard Bonichon, Julie Cailler, Olivier Hermant |
| 2021 | CCS | Search-Based Local Black-Box Deobfuscation: Understand, Improve and Mitigate (Poster). | Grgoire Menguy, Sbastien Bardin, Richard Bonichon, Cauim de Souza Lima |
| 2021 | CCS | Search-Based Local Black-Box Deobfuscation: Understand, Improve and Mitigate. | Grgoire Menguy, Sbastien Bardin, Richard Bonichon, Cauim de Souza Lima |
| 2021 | ICSE | Interface Compliance of Inline Assembly: Automatically Check, Patch and Refine. | Frdric Recoules, Sbastien Bardin, Richard Bonichon, Matthieu Lemerre, Laurent Mounier, Marie-Laure Potet |
| 2021 | ICSE | RUSTInA: Automatically Checking and Patching Inline Assembly Interface Compliance (Artifact Evaluation): Accepted submission #992 - "Interface Compliance of Inline Assembly: Automatically Check, Patch and Refine". | Frdric Recoules, Sbastien Bardin, Richard Bonichon, Matthieu Lemerre, Laurent Mounier, Marie-Laure Potet |
| 2021 | SECRYPT | Program Protection through Software-based Hardware Abstraction. | Jeffrey Todd McDonald, Ramya Manikyam, Sbastien Bardin, Richard Bonichon, Todd R. Andel |
| 2020 | RAID | Binary-level Directed Fuzzing for Use-After-Free Vulnerabilities. | Manh-Dung Nguyen, Sbastien Bardin, Richard Bonichon, Roland Groz, Matthieu Lemerre |
| 2019 | ACSAC | How to kill symbolic deobfuscation for free (or: unleashing the potential of path-oriented protections). | Mathilde Ollivier, Sbastien Bardin, Richard Bonichon, Jean-Yves Marion |
| 2018 | CAV | Model Generation for Quantified Formulas: A Taint-Based Approach. | Benjamin Farinier, Sbastien Bardin, Richard Bonichon, Marie-Laure Potet |
| 2011 | SAFECOMP | Rigorous Evidence of Freedom from Concurrency Faults in Industrial Control Software. | Richard Bonichon, Graud Canet, Loc Correnson, Eric Goubault, Emmanuel Haucourt, Michel Hirschowitz, Sbastien Labb, Samuel Mimram |
| 2009 | ICFP | Experience report: OCaml for an industrial-strength static analysis framework. | Pascal Cuoq, Julien Signoles, Patrick Baudin, Richard Bonichon, Graud Canet, Loc Correnson, Benjamin Monate, Virgile Prevosto, Armand Puccetti |
| 2007 | LPAR | Zenon : An Extensible Automated Theorem Prover Producing Checkable Proofs. | Richard Bonichon, David Delahaye, Damien Doligez |
| 2006 | LPAR | A Semantic Completeness Proof for TaMeD. | Richard Bonichon, Olivier Hermant |
| 2004 | CADE | TaMeD: A Tableau Method for Deduction Modulo. | Richard Bonichon |