Frédéric Besson

Publication Activity (10 Years)

Years Active: 1999-2024
Publications (10 Years): 18

Top Topics

Fault Isolation

Virtual Machine

Top Venues

J. Autom. Reason.

Publications

Clément Chavanon, Frédéric Besson, Tristan Ninet
PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams. CPP (2024)
Shenghao Yuan, Frédéric Besson, Jean-Pierre Talpin
End-to-End Mechanized Proof of a JIT-Accelerated eBPF Virtual Machine for IoT. CAV (1) (2024)
Nicolas Gaudin, Jean-Loup Hatchikian-Houdot, Frédéric Besson, Pascal Cotret, Guy Gogniat, Guillaume Hiet, Vianney Lapotre, Pierre Wilke
Work in Progress: Thwarting Timing Attacks in Microcontrollers using Fine-grained Hardware Protections. EuroS&P Workshops (2023)
Shenghao Yuan, Benjamin Lion, Frédéric Besson, Jean-Pierre Talpin
Making an eBPF Virtual Machine Faster on Microcontrollers: Verified Optimization and Proof Simplification. SETTA (2023)
Gautier Raimondi, Frédéric Besson, Thomas P. Jensen
Type-directed Program Transformation for Constant-Time Enforcement. PPDP (2023)
Koen Zandberg, Emmanuel Baccelli, Shenghao Yuan, Frédéric Besson, Jean-Pierre Talpin
Femto-Containers: Lightweight Virtualization and Fault Isolation For Small Software Functions on Low-Power IoT Microcontrollers. CoRR (2022)
Koen Zandberg, Emmanuel Baccelli, Shenghao Yuan, Frédéric Besson, Jean-Pierre Talpin
Femto-containers: lightweight virtualization and fault isolation for small software functions on low-power IoT microcontrollers. Middleware (2022)
Shenghao Yuan, Frédéric Besson, Jean-Pierre Talpin, Samuel Hym, Koen Zandberg, Emmanuel Baccelli
End-to-End Mechanized Proof of an eBPF Virtual Machine for Micro-controllers. CAV (2) (2022)
Frédéric Besson
Itauto: An Extensible Intuitionistic SAT Solver. ITP (2021)
Frédéric Besson, Sandrine Blazy, Alexandre Dang, Thomas P. Jensen, Pierre Wilke
Compiling Sandboxes: Formally Verified Software Fault Isolation. ESOP (2019)
Frédéric Besson, Sandrine Blazy, Pierre Wilke
CompCertS: A Memory-Aware Verified C Compiler Using a Pointer as Integer Semantics. J. Autom. Reason. 63 (2) (2019)
Frédéric Besson, Sandrine Blazy, Pierre Wilke
A Verified CompCert Front-End for a Memory Model Supporting Pointer Arithmetic and Uninitialised Data. J. Autom. Reason. 62 (4) (2019)
Frédéric Besson, Alexandre Dang, Thomas P. Jensen
Information-Flow Preservation in Compiler Optimisations. CSF (2019)
Frédéric Besson, Alexandre Dang, Thomas P. Jensen
Securing Compilation Against Memory Probing. PLAS@CCS (2018)
Frédéric Besson, Thomas P. Jensen, Julien Lepiller
Modular Software Fault Isolation as Abstract Interpretation. SAS (2018)
Frédéric Besson, Sandrine Blazy, Pierre Wilke
CompCertS: A Memory-Aware Verified C Compiler Using Pointer as Integer Semantics. ITP (2017)
Frédéric Besson, Nataliia Bielova, Thomas P. Jensen
Hybrid Monitoring of Attacker Knowledge. CSF (2016)
Nataliia Bielova, Frédéric Besson, Thomas P. Jensen
Using JavaScript Monitoring to Prevent Device Fingerprinting. ERCIM News 2016 (106) (2016)
Frédéric Besson, Sandrine Blazy, Pierre Wilke
A Concrete Memory Model for CompCert. ITP (2015)
Frédéric Besson, Thomas P. Jensen, Pierre Vittet
SawjaCard: A Static Analysis Tool for Certifying Java Card Applications. SAS (2014)
Frédéric Besson, Nataliia Bielova, Thomas P. Jensen
Browser Randomisation against Fingerprinting: A Quantitative Information Flow Approach. NordSec (2014)
Frédéric Besson, Sandrine Blazy, Pierre Wilke
A Precise and Abstract Memory Model for C Using Symbolic Values. APLAS (2014)
Frédéric Besson, Pierre-Emmanuel Cornilleau, Thomas P. Jensen
Result Certification of Static Program Analysers with Automated Theorem Provers. VSTTE (2013)
Frédéric Besson, Nataliia Bielova, Thomas P. Jensen
Hybrid Information Flow Monitoring against Web Tracking. CSF (2013)
Frédéric Besson, Pierre-Emmanuel Cornilleau, Ronan Saillard
Walking through the Forest: Fast EUF Proof-Checking Algorithms. PxTP (2012)
Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie
Modular SMT Proofs for Fast Reflexive Checking Inside Coq. CPP (2011)
Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie
A Nelson-Oppen based Proof System using Theory Specific Proof Systems. PxTP (2011)
Frédéric Besson, Pascal Fontaine, Laurent Théry
A Flexible Proof Format for SMT: a Proposal. PxTP (2011)
Laurent Hubert, Nicolas Barré, Frédéric Besson, Delphine Demange, Thomas P. Jensen, Vincent Monfort, David Pichardie, Tiphaine Turpin
Sawja: Static Analysis Workshop for Java CoRR (2010)
Frédéric Besson, Guillaume Dufay, Thomas P. Jensen, David Pichardie
Verifying resource access control on mobile interactive devices. J. Comput. Secur. 18 (6) (2010)
Frédéric Besson, Thomas P. Jensen, David Pichardie, Tiphaine Turpin
Certified Result Checking for Polyhedral Analysis of Bytecode Programs. TGC (2010)
Laurent Hubert, Nicolas Barré, Frédéric Besson, Delphine Demange, Thomas P. Jensen, Vincent Monfort, David Pichardie, Tiphaine Turpin
Sawja: Static Analysis Workshop for Java. FoVeOOS (2010)
Frédéric Besson
CPA beats ∞-CFA. FTfJP@ECOOP (2009)
Frédéric Besson, David Cachera, Thomas P. Jensen, David Pichardie
Certified Static Analysis by Abstract Interpretation. FOSAD (2009)
Frédéric Besson, Thomas P. Jensen, Tiphaine Turpin
Computing Stack Maps with Interfaces. ECOOP (2008)
Frédéric Besson, Thomas P. Jensen, Tiphaine Turpin
Small Witnesses for Abstract Interpretation-Based Proofs. ESOP (2007)
Frédéric Besson
Fast Reflexive Arithmetic Tactics the Linear Case and Beyond. TYPES (2006)
Frédéric Besson, Guillaume Dufay, Thomas P. Jensen
A Formal Model of Access Control for Mobile Interactive Devices. ESORICS (2006)
Frédéric Besson, Thomas P. Jensen, David Pichardie
Proof-carrying code from certified abstract interpretation and fixpoint compression. Theor. Comput. Sci. 364 (3) (2006)
Frédéric Besson, Thomas de Grenier de Latour, Thomas P. Jensen
Interfaces for stack inspection. J. Funct. Program. 15 (2) (2005)
Frédéric Besson, Tomasz Blanc, Cédric Fournet, Andrew D. Gordon
From Stack Inspection to Access Control: A Security Analysis for Libraries. CSFW (2004)
Frédéric Besson, Thomas P. Jensen
Modular Class Analysis with DATALOG. SAS (2003)
Frédéric Besson, Thomas de Grenier de Latour, Thomas P. Jensen
Secure calling contexts for stack inspection. PPDP (2002)
Frédéric Besson, Thomas P. Jensen, Daniel Le Métayer
Model Checking Security Properties of Control Flow Graphs. J. Comput. Secur. 9 (3) (2001)
Frédéric Besson, Thomas P. Jensen, Jean-Pierre Talpin
Polyhedral Analysis for Synchronous Languages. SAS (1999)