Frédéric Besson

According to our database, Frédéric Besson authored at least 43 papers between 1999 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

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

Proceedings of the Computer Security - ESORICS 2024, 2024

PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams.

Clément Chavanon, Frédéric Besson, Tristan Ninet

Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2024

End-to-End Mechanized Proof of a JIT-Accelerated eBPF Virtual Machine for IoT.

Shenghao Yuan, Frédéric Besson, Jean-Pierre Talpin

Proceedings of the Computer Aided Verification - 36th International Conference, 2024

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

Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2023

Type-directed Program Transformation for Constant-Time Enforcement.

Gautier Raimondi, Frédéric Besson, Thomas P. Jensen

Proceedings of the International Symposium on Principles and Practice of Declarative Programming, 2023

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

Proceedings of the IEEE European Symposium on Security and Privacy, 2023

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

Proceedings of the Middleware '22: 23rd International Middleware Conference, Quebec, QC, Canada, November 7, 2022

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

Proceedings of the Computer Aided Verification - 34th International Conference, 2022

2021

Itauto: An Extensible Intuitionistic SAT Solver.

Frédéric Besson

Proceedings of the 12th International Conference on Interactive Theorem Proving, 2021

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

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

Compiling Sandboxes: Formally Verified Software Fault Isolation.

Frédéric Besson, Sandrine Blazy, Alexandre Dang, Thomas P. Jensen, Pierre Wilke

Proceedings of the Programming Languages and Systems, 2019

Information-Flow Preservation in Compiler Optimisations.

Frédéric Besson, Alexandre Dang, Thomas P. Jensen

Proceedings of the 32nd IEEE Computer Security Foundations Symposium, 2019

2018

Modular Software Fault Isolation as Abstract Interpretation.

Frédéric Besson, Thomas P. Jensen, Julien Lepiller

Proceedings of the Static Analysis - 25th International Symposium, 2018

Securing Compilation Against Memory Probing.

Frédéric Besson, Alexandre Dang, Thomas P. Jensen

Proceedings of the 13th Workshop on Programming Languages and Analysis for Security, 2018

2016

Using JavaScript Monitoring to Prevent Device Fingerprinting.

Nataliia Bielova, Frédéric Besson, Thomas P. Jensen

ERCIM News, 2016

Hybrid Monitoring of Attacker Knowledge.

Frédéric Besson, Nataliia Bielova, Thomas P. Jensen

Proceedings of the IEEE 29th Computer Security Foundations Symposium, 2016

2015

A Concrete Memory Model for CompCert.

Frédéric Besson, Sandrine Blazy, Pierre Wilke

Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

2014

SawjaCard: A Static Analysis Tool for Certifying Java Card Applications.

Frédéric Besson, Thomas P. Jensen, Pierre Vittet

Proceedings of the Static Analysis - 21st International Symposium, 2014

Browser Randomisation against Fingerprinting: A Quantitative Information Flow Approach.

Frédéric Besson, Nataliia Bielova, Thomas P. Jensen

Proceedings of the Secure IT Systems - 19th Nordic Conference, NordSec 2014, Tromsø, 2014

A Precise and Abstract Memory Model for C Using Symbolic Values.

Frédéric Besson, Sandrine Blazy, Pierre Wilke

Proceedings of the Programming Languages and Systems - 12th Asian Symposium, 2014

2013

Result Certification of Static Program Analysers with Automated Theorem Provers.

Frédéric Besson, Pierre-Emmanuel Cornilleau, Thomas P. Jensen

Proceedings of the Verified Software: Theories, Tools, Experiments, 2013

Hybrid Information Flow Monitoring against Web Tracking.

Frédéric Besson, Nataliia Bielova, Thomas P. Jensen

Proceedings of the 2013 IEEE 26th Computer Security Foundations Symposium, 2013

2012

Walking through the Forest: Fast EUF Proof-Checking Algorithms.

Frédéric Besson, Pierre-Emmanuel Cornilleau, Ronan Saillard

Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving, 2012

2011

A Flexible Proof Format for SMT: a Proposal.

Frédéric Besson, Pascal Fontaine, Laurent Théry

Proceedings of the PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving, 2011

A Nelson-Oppen based Proof System using Theory Specific Proof Systems.

Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie

Proceedings of the PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving, 2011

Modular SMT Proofs for Fast Reflexive Checking Inside Coq.

Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie

Proceedings of the Certified Programs and Proofs - First International Conference, 2011

2010

Verifying resource access control on mobile interactive devices.

Frédéric Besson, Guillaume Dufay, Thomas P. Jensen, David Pichardie

J. Comput. Secur., 2010

Certified Result Checking for Polyhedral Analysis of Bytecode Programs.

Frédéric Besson, Thomas P. Jensen, David Pichardie, Tiphaine Turpin

Proceedings of the Trustworthly Global Computing - 5th International Symposium, 2010

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

Proceedings of the Formal Verification of Object-Oriented Software, 2010

2009

Certified Static Analysis by Abstract Interpretation.

Frédéric Besson, David Cachera, Thomas P. Jensen, David Pichardie

Proceedings of the Foundations of Security Analysis and Design V, 2009

CPA beats ∞-CFA.

Frédéric Besson

Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs, 2009

2008

Computing Stack Maps with Interfaces.

Frédéric Besson, Thomas P. Jensen, Tiphaine Turpin

Proceedings of the ECOOP 2008, 2008

2007

Small Witnesses for Abstract Interpretation-Based Proofs.

Frédéric Besson, Thomas P. Jensen, Tiphaine Turpin

Proceedings of the Programming Languages and Systems, 2007

2006

Proof-carrying code from certified abstract interpretation and fixpoint compression.

Frédéric Besson, Thomas P. Jensen, David Pichardie

Theor. Comput. Sci., 2006

Fast Reflexive Arithmetic Tactics the Linear Case and Beyond.

Frédéric Besson

Proceedings of the Types for Proofs and Programs, International Workshop, 2006

A Formal Model of Access Control for Mobile Interactive Devices.

Frédéric Besson, Guillaume Dufay, Thomas P. Jensen

Proceedings of the Computer Security, 2006

2005

Interfaces for stack inspection.

Frédéric Besson, Thomas de Grenier de Latour, Thomas P. Jensen

J. Funct. Program., 2005

2004

From Stack Inspection to Access Control: A Security Analysis for Libraries.

Frédéric Besson, Tomasz Blanc, Cédric Fournet, Andrew D. Gordon

Proceedings of the 17th IEEE Computer Security Foundations Workshop, 2004

2003

Modular Class Analysis with DATALOG.

Frédéric Besson, Thomas P. Jensen

Proceedings of the Static Analysis, 10th International Symposium, 2003

2002

Secure calling contexts for stack inspection.

Frédéric Besson, Thomas de Grenier de Latour, Thomas P. Jensen

Proceedings of the 4th international ACM SIGPLAN conference on Principles and practice of declarative programming, 2002

2001

Model Checking Security Properties of Control Flow Graphs.

Frédéric Besson, Thomas P. Jensen, Daniel Le Métayer

J. Comput. Secur., 2001

1999

Polyhedral Analysis for Synchronous Languages.

Frédéric Besson, Thomas P. Jensen, Jean-Pierre Talpin

Proceedings of the Static Analysis, 6th International Symposium, 1999