Polyhedral Analysis for Synchronous Languages. - Frédéric Besson; Thomas P. Jensen; Jean-Pierre Talpin (SAS, 1999)

Model Checking Security Properties of Control Flow Graphs. - Frédéric Besson; Thomas P. Jensen; Daniel Le Métayer (J. Comput. Secur., 2001)

Secure calling contexts for stack inspection. - Frédéric Besson; Thomas de Grenier de Latour; Thomas P. Jensen (PPDP, 2002)

Modular Class Analysis with DATALOG. - Frédéric Besson; Thomas P. Jensen (SAS, 2003)

From Stack Inspection to Access Control: A Security Analysis for Libraries. - Frédéric Besson; Tomasz Blanc; Cédric Fournet; Andrew D. Gordon 001 (CSFW, 2004)

Interfaces for stack inspection. - Frédéric Besson; Thomas de Grenier de Latour; Thomas P. Jensen (J. Funct. Program., 2005)

A Formal Model of Access Control for Mobile Interactive Devices. - Frédéric Besson; Guillaume Dufay; Thomas P. Jensen (ESORICS, 2006)

Fast Reflexive Arithmetic Tactics the Linear Case and Beyond. - Frédéric Besson (TYPES, 2006)

Proof-carrying code from certified abstract interpretation and fixpoint compression. - Frédéric Besson; Thomas P. Jensen; David Pichardie (Theor. Comput. Sci., 2006)

Small Witnesses for Abstract Interpretation-Based Proofs. - Frédéric Besson; Thomas P. Jensen; Tiphaine Turpin (ESOP, 2007)

Computing Stack Maps with Interfaces. - Frédéric Besson; Thomas P. Jensen; Tiphaine Turpin (ECOOP, 2008)

CPA beats ∞-CFA. - Frédéric Besson (FTfJP@ECOOP, 2009)

Certified Static Analysis by Abstract Interpretation. - Frédéric Besson; David Cachera; Thomas P. Jensen; David Pichardie (FOSAD, 2009)

Sawja: Static Analysis Workshop for Java. - Laurent Hubert; Nicolas Barré; Frédéric Besson; Delphine Demange; Thomas P. Jensen; Vincent Monfort; David Pichardie; Tiphaine Turpin (FoVeOOS, 2010)

Certified Result Checking for Polyhedral Analysis of Bytecode Programs. - Frédéric Besson; Thomas P. Jensen; David Pichardie; Tiphaine Turpin (TGC, 2010)

Verifying resource access control on mobile interactive devices. - Frédéric Besson; Guillaume Dufay; Thomas P. Jensen; David Pichardie (J. Comput. Secur., 2010)

Modular SMT Proofs for Fast Reflexive Checking Inside Coq. - Frédéric Besson; Pierre-Emmanuel Cornilleau; David Pichardie (CPP, 2011)

A Nelson-Oppen based Proof System using Theory Specific Proof Systems. - Frédéric Besson; Pierre-Emmanuel Cornilleau; David Pichardie (PxTP, 2011)

A Flexible Proof Format for SMT: a Proposal. - Frédéric Besson; Pascal Fontaine; Laurent Théry (PxTP, 2011)

Walking through the Forest: Fast EUF Proof-Checking Algorithms. - Frédéric Besson; Pierre-Emmanuel Cornilleau; Ronan Saillard (PxTP, 2012)

Hybrid Information Flow Monitoring against Web Tracking. - Frédéric Besson; Nataliia Bielova; Thomas P. Jensen (CSF, 2013)

Result Certification of Static Program Analysers with Automated Theorem Provers. - Frédéric Besson; Pierre-Emmanuel Cornilleau; Thomas P. Jensen (VSTTE, 2013)

A Precise and Abstract Memory Model for C Using Symbolic Values. - Frédéric Besson; Sandrine Blazy; Pierre Wilke (APLAS, 2014)

Browser Randomisation against Fingerprinting: A Quantitative Information Flow Approach. - Frédéric Besson; Nataliia Bielova; Thomas P. Jensen (NordSec, 2014)

SawjaCard: A Static Analysis Tool for Certifying Java Card Applications. - Frédéric Besson; Thomas P. Jensen; Pierre Vittet (SAS, 2014)

A Concrete Memory Model for CompCert. - Frédéric Besson; Sandrine Blazy; Pierre Wilke (ITP, 2015)

Hybrid Monitoring of Attacker Knowledge. - Frédéric Besson; Nataliia Bielova; Thomas P. Jensen (CSF, 2016)

Using JavaScript Monitoring to Prevent Device Fingerprinting. - Nataliia Bielova; Frédéric Besson; Thomas P. Jensen (ERCIM News, 2016)

Securing Compilation Against Memory Probing. - Frédéric Besson; Alexandre Dang; Thomas P. Jensen (PLAS@CCS, 2018)

Modular Software Fault Isolation as Abstract Interpretation. - Frédéric Besson; Thomas P. Jensen; Julien Lepiller (SAS, 2018)

Information-Flow Preservation in Compiler Optimisations. - Frédéric Besson; Alexandre Dang; Thomas P. Jensen (CSF, 2019)

Compiling Sandboxes: Formally Verified Software Fault Isolation. - Frédéric Besson; Sandrine Blazy; Alexandre Dang; Thomas P. Jensen; Pierre Wilke (ESOP, 2019)

A Verified CompCert Front-End for a Memory Model Supporting Pointer Arithmetic and Uninitialised Data. - Frédéric Besson; Sandrine Blazy; Pierre Wilke (J. Autom. Reason., 2019)

CompCertS: A Memory-Aware Verified C Compiler Using a Pointer as Integer Semantics. - Frédéric Besson; Sandrine Blazy; Pierre Wilke (J. Autom. Reason., 2019)

Itauto: An Extensible Intuitionistic SAT Solver. - Frédéric Besson (ITP, 2021)

End-to-End Mechanized Proof of an eBPF Virtual Machine for Micro-controllers. - Shenghao Yuan; Frédéric Besson; Jean-Pierre Talpin; Samuel Hym; Koen Zandberg; Emmanuel Baccelli (CAV (2), 2022)

Femto-containers: lightweight virtualization and fault isolation for small software functions on low-power IoT microcontrollers. - Koen Zandberg; Emmanuel Baccelli; Shenghao Yuan; Frédéric Besson; Jean-Pierre Talpin (Middleware, 2022)

Work in Progress: Thwarting Timing Attacks in Microcontrollers using Fine-grained Hardware Protections. - Nicolas Gaudin; Jean-Loup Hatchikian-Houdot; Frédéric Besson; Pascal Cotret; Guy Gogniat; Guillaume Hiet; Vianney Lapotre; Pierre Wilke (EuroS&P Workshops, 2023)

Type-directed Program Transformation for Constant-Time Enforcement. - Gautier Raimondi; Frédéric Besson; Thomas P. Jensen (PPDP, 2023)

Making an eBPF Virtual Machine Faster on Microcontrollers: Verified Optimization and Proof Simplification. - Shenghao Yuan; Benjamin Lion; Frédéric Besson; Jean-Pierre Talpin (SETTA, 2023)

End-to-End Mechanized Proof of a JIT-Accelerated eBPF Virtual Machine for IoT. - Shenghao Yuan; Frédéric Besson; Jean-Pierre Talpin (CAV (1), 2024)

PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams. - Clément Chavanon; Frédéric Besson; Tristan Ninet (CPP, 2024)

Formal Hardware/Software Models for Cache Locking Enabling Fast and Secure Code. - Jean-Loup Hatchikian-Houdot; Pierre Wilke; Frédéric Besson; Guillaume Hiet (ESORICS (3), 2024)

Side-Channel Resistant Applications through Co-designed Hardware/ Software: the SCRATCHS Project. - Frédéric Besson; Célia Le Du; Pierre Wilke (ERCIM News, 2024)

BeePL: Correct-by-compilation kernel extensions. - Swarn Priya; Frédéric Besson; Connor Sughrue; Tim Steenvoorden; Jamie Fulford; Freek Verbeek; Binoy Ravindran (CoRR, 2025)