Frédéric Besson

48 papers A 8B 10C 2Misc 1Journal 11Unranked 16

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