| 2024 | CAV | End-to-End Mechanized Proof of a JIT-Accelerated eBPF Virtual Machine for IoT. | Shenghao Yuan, Frdric Besson, Jean-Pierre Talpin |
| 2024 | CPP | PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams. | Clment Chavanon, Frdric Besson, Tristan Ninet |
| 2024 | ESORICS | Formal Hardware/Software Models for Cache Locking Enabling Fast and Secure Code. | Jean-Loup Hatchikian-Houdot, Pierre Wilke, Frdric Besson, Guillaume Hiet |
| 2023 | PPDP | Type-directed Program Transformation for Constant-Time Enforcement. | Gautier Raimondi, Frdric Besson, Thomas P. Jensen |
| 2023 | SETTA | Making an eBPF Virtual Machine Faster on Microcontrollers: Verified Optimization and Proof Simplification. | Shenghao Yuan, Benjamin Lion, Frdric Besson, Jean-Pierre Talpin |
| 2022 | CAV | End-to-End Mechanized Proof of an eBPF Virtual Machine for Micro-controllers. | Shenghao Yuan, Frdric Besson, Jean-Pierre Talpin, Samuel Hym, Koen Zandberg, Emmanuel Baccelli |
| 2022 | Middleware | Femto-containers: lightweight virtualization and fault isolation for small software functions on low-power IoT microcontrollers. | Koen Zandberg, Emmanuel Baccelli, Shenghao Yuan, Frdric Besson, Jean-Pierre Talpin |
| 2021 | ITP | Itauto: An Extensible Intuitionistic SAT Solver. | Frdric Besson |
| 2019 | ESOP | Compiling Sandboxes: Formally Verified Software Fault Isolation. | Frdric Besson, Sandrine Blazy, Alexandre Dang, Thomas P. Jensen, Pierre Wilke |
| 2018 | CCS | Securing Compilation Against Memory Probing. | Frdric Besson, Alexandre Dang, Thomas P. Jensen |
| 2018 | SAS | Modular Software Fault Isolation as Abstract Interpretation. | Frdric Besson, Thomas P. Jensen, Julien Lepiller |
| 2017 | ITP | CompCertS: A Memory-Aware Verified C Compiler Using Pointer as Integer Semantics. | Frdric Besson, Sandrine Blazy, Pierre Wilke |
| 2015 | ITP | A Concrete Memory Model for CompCert. | Frdric Besson, Sandrine Blazy, Pierre Wilke |
| 2014 | APLAS | A Precise and Abstract Memory Model for C Using Symbolic Values. | Frdric Besson, Sandrine Blazy, Pierre Wilke |
| 2014 | SAS | SawjaCard: A Static Analysis Tool for Certifying Java Card Applications. | Frdric Besson, Thomas P. Jensen, Pierre Vittet |
| 2011 | CPP | Modular SMT Proofs for Fast Reflexive Checking Inside Coq. | Frdric Besson, Pierre-Emmanuel Cornilleau, David Pichardie |
| 2009 | ECOOP | CPA beats ∞-CFA. | Frdric Besson |
| 2008 | ECOOP | Computing Stack Maps with Interfaces. | Frdric Besson, Thomas P. Jensen, Tiphaine Turpin |
| 2007 | ESOP | Small Witnesses for Abstract Interpretation-Based Proofs. | Frdric Besson, Thomas P. Jensen, Tiphaine Turpin |
| 2006 | ESORICS | A Formal Model of Access Control for Mobile Interactive Devices. | Frdric Besson, Guillaume Dufay, Thomas P. Jensen |
| 2003 | SAS | Modular Class Analysis with DATALOG. | Frdric Besson, Thomas P. Jensen |
| 2002 | PPDP | Secure calling contexts for stack inspection. | Frdric Besson, Thomas de Grenier de Latour, Thomas P. Jensen |
| 1999 | SAS | Polyhedral Analysis for Synchronous Languages. | Frdric Besson, Thomas P. Jensen, Jean-Pierre Talpin |