TaMeD: A Tableau Method for Deduction Modulo. - Richard Bonichon (IJCAR, 2004)

A Semantic Completeness Proof for TaMeD. - Richard Bonichon; Olivier Hermant (LPAR, 2006)

On Constructive Cut Admissibility in Deduction Modulo. - Richard Bonichon; Olivier Hermant (TYPES, 2006)

Zenon : An Extensible Automated Theorem Prover Producing Checkable Proofs. - Richard Bonichon; David Delahaye; Damien Doligez (LPAR, 2007)

Experience report: OCaml for an industrial-strength static analysis framework. - Pascal Cuoq; Julien Signoles; Patrick Baudin; Richard Bonichon; Géraud Canet; Loïc Correnson; Benjamin Monate; Virgile Prevosto; Armand Puccetti (ICFP, 2009)

Rigorous Evidence of Freedom from Concurrency Faults in Industrial Control Software. - Richard Bonichon; Géraud Canet; Loïc Correnson; Eric Goubault; Emmanuel Haucourt; Michel Hirschowitz; Sébastien Labbé 002; Samuel Mimram (SAFECOMP, 2011)

A Mergeable Interval Map. - Richard Bonichon; Pascal Cuoq (Stud. Inform. Univ., 2011)

LLVM-Based Code Generation for B. - Richard Bonichon; David Déharbe; Thierry Lecomte; Valério Medeiros Jr. (SBMF, 2014)

Extending SMT-LIB v2 with λ-Terms and Polymorphism. - Richard Bonichon; David Déharbe; Cláudia Tavares (SMT, 2014)

A syntactic soundness proof for free-variable tableaux with on-the-fly Skolemization. - Richard Bonichon; Olivier Hermant (CoRR, 2015)

Model Generation for Quantified Formulas: A Taint-Based Approach. - Benjamin Farinier; Sébastien Bardin; Richard Bonichon; Marie-Laure Potet (CAV (2), 2018)

How to kill symbolic deobfuscation for free (or: unleashing the potential of path-oriented protections). - Mathilde Ollivier; Sébastien Bardin; Richard Bonichon; Jean-Yves Marion (ACSAC, 2019)

Get Rid of Inline Assembly through Verification-Oriented Lifting. - Frédéric Recoules; Sébastien Bardin; Richard Bonichon; Laurent Mounier; Marie-Laure Potet (ASE, 2019)

Get rid of inline assembly through trustable verification-oriented lifting. - Frédéric Recoules; Sébastien Bardin; Richard Bonichon; Laurent Mounier; Marie-Laure Potet (CoRR, 2019)

Binary-level Directed Fuzzing for Use-After-Free Vulnerabilities. - Manh-Dung Nguyen; Sébastien Bardin; Richard Bonichon; Roland Groz; Matthieu Lemerre (RAID, 2020)

Search-Based Local Black-Box Deobfuscation: Understand, Improve and Mitigate (Poster). - Grégoire Menguy; Sébastien Bardin; Richard Bonichon; Cauim de Souza Lima (CCS, 2021)

Search-Based Local Black-Box Deobfuscation: Understand, Improve and Mitigate. - Grégoire Menguy; Sébastien Bardin; Richard Bonichon; Cauim de Souza Lima (CCS, 2021)

Evaluating Defensive Countermeasures for Software-Based Hardware Abstraction. - Jeffrey Todd McDonald; Ramya K. Manikyam; Sébastien Bardin; Richard Bonichon; Todd R. Andel; James Carambat (ICETE (Selected Papers), 2021)

Interface Compliance of Inline Assembly: Automatically Check, Patch and Refine. - Frédéric Recoules; Sébastien Bardin; Richard Bonichon; Matthieu Lemerre; Laurent Mounier; Marie-Laure Potet (ICSE, 2021)

RUSTInA: Automatically Checking and Patching Inline Assembly Interface Compliance (Artifact Evaluation): Accepted submission #992 - "Interface Compliance of Inline Assembly: Automatically Check, Patch and Refine". - Frédéric Recoules; Sébastien Bardin; Richard Bonichon; Matthieu Lemerre; Laurent Mounier; Marie-Laure Potet (ICSE (Companion Volume), 2021)

Program Protection through Software-based Hardware Abstraction. - Jeffrey Todd McDonald; Ramya Manikyam; Sébastien Bardin; Richard Bonichon; Todd R. Andel (SECRYPT, 2021)

AI-based Blackbox Code Deobfuscation: Understand, Improve and Mitigate. - Grégoire Menguy; Sébastien Bardin; Richard Bonichon; Cauim de Souza Lima (CoRR, 2021)

A Generic Deskolemization Strategy. - Johann Rosain; Richard Bonichon; Julie Cailler; Olivier Hermant (LPAR, 2024)