Journal articles
2019
- titre
- CompCertS: A Memory-Aware Verified C Compiler using a Pointer as Integer Semantics
- auteur
- Frédéric Besson, Sandrine Blazy, Pierre Wilke
- article
- Journal of Automated Reasoning, 2019, 63 (2), pp.369-392. ⟨10.1007/s10817-018-9496-y⟩
- Accès au texte intégral et bibtex
-
- titre
- A Verified CompCert Front-End for a Memory Model Supporting Pointer Arithmetic and Uninitialised Data
- auteur
- Frédéric Besson, Sandrine Blazy, Pierre Wilke
- article
- Journal of Automated Reasoning, 2019, 62 (4), pp.433-480. ⟨10.1007/s10817-017-9439-z⟩
- Accès au texte intégral et bibtex
-
2010
- titre
- Verifying Resource Access Control on Mobile Interactive Devices
- auteur
- Frédéric Besson, Guillaume Dufaye, Thomas Jensen, David Pichardie
- article
- Journal of Computer Security, 2010, 18 (6), pp.971-998
- Accès au texte intégral et bibtex
-
Conference papers
2023
- titre
- Making an eBPF Virtual Machine Faster on Microcontrollers: Verified Optimization and Proof Simplification
- auteur
- Shenghao Yuan, Benjamin Lion, Frédéric Besson, Jean-Pierre Talpin
- article
- SETTA 2023 - 9th International Symposium Dependable Software Engineering. Theories, Tools, and Applications, Nov 2023, Nanjing (Chine), China. pp.385-401, ⟨10.1007/978-981-99-8664-4_22⟩
- Accès au texte intégral et bibtex
-
- titre
- Type-directed Program Transformation for Constant-Time Enforcement
- auteur
- Frédéric Besson, Thomas Jensen, Gautier Raimondi
- article
- PPDP 2023 - International Symposium on Principles and Practice of Declarative Programming, Oct 2023, Lisboa, Portugal. pp.1-13, ⟨10.1145/3610612.3610618⟩
- Accès au texte intégral et bibtex
-
2022
- titre
- Femto-Containers: Lightweight Virtualization and Fault Isolation For Small Software Functions on Low-Power IoT Microcontrollers
- auteur
- Koen Zandberg, Emmanuel Baccelli, Shenghao Yuan, Frédéric Besson, Jean-Pierre Talpin
- article
- Middleware 2022 - 23rd ACM/IFIP International Conference Middleware, Nov 2022, Quebec, Canada. pp.1-12, ⟨10.1145/3528535.3565242⟩
- Accès au texte intégral et bibtex
-
- titre
- End-to-end Mechanized Proof of an eBPF Virtual Machine for Micro-controllers
- auteur
- Shenghao Yuan, Frédéric Besson, Jean-Pierre Talpin, Samuel Hym, Koen Zandberg, Emmanuel Baccelli
- article
- CAV 2022 - 34th International Conference on Computer Aided Verification, Aug 2022, Haifa, Israel. pp.1-23
- Accès au texte intégral et bibtex
-
2021
- titre
- Itauto: An Extensible Intuitionistic SAT Solver
- auteur
- Frédéric Besson
- article
- ITP 2021 - 12th International Conference on Interactive Theorem Proving, Jun 2021, Roma, Italy. pp.1-18, ⟨10.4230/LIPIcs.ITP.2021.9⟩
- Accès au texte intégral et bibtex
-
2019
- titre
- Information-Flow Preservation in Compiler Optimisations
- auteur
- Frédéric Besson, Alexandre Dang, Thomas Jensen
- article
- CSF 2019 - 32nd IEEE Computer Security Foundations Symposium, Jun 2019, Hoboken, United States. pp.1-13
- Accès au texte intégral et bibtex
-
- titre
- Compiling Sandboxes: Formally Verified Software Fault Isolation
- auteur
- Frédéric Besson, Sandrine Blazy, Alexandre Dang, Thomas Jensen, Pierre Wilke
- article
- ESOP 2019 - 28th European Symposium on Programming, Apr 2019, Prague, Czech Republic. pp.499-524, ⟨10.1007/978-3-030-17184-1_18⟩
- Accès au texte intégral et bibtex
-
2018
- titre
- Securing Compilation Against Memory Probing
- auteur
- Frédéric Besson, Alexandre Dang, Thomas Jensen
- article
- PLAS '18 - 13th Workshop on Programming Languages and Analysis for Security, Oct 2018, Toronto, Canada. pp.29-40, ⟨10.1145/3264820.3264822⟩
- Accès au texte intégral et bibtex
-
- titre
- Modular Software Fault Isolation as Abstract Interpretation
- auteur
- Frédéric Besson, Thomas Jensen, Julien Lepiller
- article
- SAS 2018 - 25th International Static Analysis Symposium, Aug 2018, Freiburg, Germany. pp.166-186, ⟨10.1007/978-3-319-99725-4_12⟩
- Accès au texte intégral et bibtex
-
2017
- titre
- CompCertS: A Memory-Aware Verified C Compiler using Pointer as Integer Semantics
- auteur
- Frédéric Besson, Sandrine Blazy, Pierre Wilke
- article
- ITP 2017 - 8th International Conference on Interactive Theorem Proving, Sep 2017, Brasilia, Brazil. pp.81-97, ⟨10.1007/978-3-319-66107-0_6⟩
- Accès au texte intégral et bibtex
-
- titre
- Confusion de Type en C++: État de l'Art et Difficultés de Détection
- auteur
- Florent Saudel, Sandrine Blazy, Frédéric Besson
- article
- RESSI 2017 - Rendez-vous de la Recherche et de l'Enseignement de la Sécurité des Systèmes d'Information , May 2017, Grenoble/Autrans, France. pp.1-5
- Accès au texte intégral et bibtex
-
2016
- titre
- Hybrid Monitoring of Attacker Knowledge
- auteur
- Frédéric Besson, Nataliia Bielova, Thomas Jensen
- article
- 29th IEEE Computer Security Foundations Symposium, 2016, Lisboa, Portugal
- Accès au texte intégral et bibtex
-
2015
- titre
- A Concrete Memory Model for CompCert
- auteur
- Frédéric Besson, Sandrine Blazy, Pierre Wilke
- article
- ITP 2015 : 6th International Conference on Interactive Theorem Proving, Aug 2015, Nanjing, China. pp.67-83, ⟨10.1007/978-3-319-22102-1_5⟩
- Accès au texte intégral et bibtex
-
2014
- titre
- Browser Randomisation against Fingerprinting: A Quantitative Information Flow Approach
- auteur
- Frédéric Besson, Nataliia Bielova, Thomas Jensen
- article
- Nordic Conference on Secure IT Systems (NordSec 2014), Oct 2014, Tromsø, Norway. ⟨10.1007/978-3-319-11599-3_11⟩
- Accès au texte intégral et bibtex
-
- titre
- SawjaCard: A Static Analysis Tool for Certifying Java Card Applications
- auteur
- Frédéric Besson, Thomas Jensen, Pierre Vittet
- article
- 21st International Static Analysis Symposium (SAS 2014), 2014, Munich, Germany. pp.51 - 67, ⟨10.1007/978-3-319-10936-7_4⟩
- Accès au texte intégral et bibtex
-
- titre
- A Precise and Abstract Memory Model for C Using Symbolic Values
- auteur
- Frédéric Besson, Sandrine Blazy, Pierre Wilke
- article
- 12th Asian Symposium on Programming Languages and Systems (APLAS 2014), 2014, Singapore, Singapore. pp.449 - 468, ⟨10.1007/978-3-319-12736-1_24⟩
- Accès au texte intégral et bibtex
-
2013
- titre
- Hybrid Information Flow Monitoring Against Web Tracking
- auteur
- Frédéric Besson, Nataliia Bielova, Thomas Jensen
- article
- CSF - 2013 IEEE 26th Computer Security Foundations Symposium, 2013, New Orleans, United States. ⟨10.1109/CSF.2013.23⟩
- Accès au texte intégral et bibtex
-
- titre
- Result Certification of Static Program Analysers with Automated Theorem Provers
- auteur
- Frédéric Besson, Pierre-Emmanuel Cornilleau, Thomas Jensen
- article
- VSTTE 2013 - Fifth Working Conference on Verified Software: Theories, Tools and Experiments, 2013, Atherthon, United States
- Accès au texte intégral et bibtex
-
2011
- titre
- A Nelson-Oppen based Proof System using Theory Specific Proof Systems
- auteur
- Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie
- article
- First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland
- Accès au texte intégral et bibtex
-
- titre
- A Flexible Proof Format for SMT: a Proposal
- auteur
- Frédéric Besson, Pascal Fontaine, Laurent Théry
- article
- First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland
- Accès au texte intégral et bibtex
-
- titre
- Modular SMT Proofs for Fast Reflexive Checking inside Coq
- auteur
- Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie
- article
- First International Conference on Certified Programs and Proofs, 2011, Kenting, Taiwan
- Accès au texte intégral et bibtex
-
2010
- titre
- Sawja: Static Analysis Workshop for Java
- auteur
- Laurent Hubert, Nicolas Barré, Frédéric Besson, Delphine Demange, Thomas Jensen, Vincent Monfort, David Pichardie, Tiphaine Turpin
- article
- The International Conference on Formal Verification of Object-Oriented Software, Beckert, Bernhard and Marché, Claude, 2010, Paris, France. pp.253--267
- Accès au texte intégral et bibtex
-
- titre
- Certified Result Checking for Polyhedral Analysis of Bytecode Programs
- auteur
- Frédéric Besson, Thomas Jensen, David Pichardie, Tiphaine Turpin
- article
- The 5th International Symposium on Trustworthy Global Computing (TGC), 2010, Munich, Germany
- Accès au texte intégral et bibtex
-
- titre
- On using an inexact floating-point LP solver for deciding linear arithmetic in an SMT solver
- auteur
- Frédéric Besson
- article
- 8th International Workshop on Satisfiability Modulo Theories, 2010, Edinburgh, United Kingdom
- Accès au texte intégral et bibtex
-
2009
- titre
- CPA beats oo-CFA
- auteur
- Frédéric Besson
- article
- FTfJP '09 - Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs, 2009, Genova, Italy. ⟨10.1145/1557898.1557905⟩
- Accès au texte intégral et bibtex
-
- titre
- Certified Static Analysis by Abstract Interpretation
- auteur
- Frédéric Besson, David Cachera, Thomas Jensen, David Pichardie
- article
- Foundations of Security Analysis and Design V (FOSAD), 2009, Bertinoro, Italy. pp.223-257
- Accès au texte intégral et bibtex
-
2008
- titre
- Computing stack maps with interfaces
- auteur
- Frédéric Besson, Thomas Jensen, Tiphaine Turpin
- article
- ECOOP'08, 2008, Paphos, Cyprus
- Accès au texte intégral et bibtex
-
1999
- titre
- Polyhedral Analysis for Synchronous Languages
- auteur
- Frédéric Besson, Thomas Jensen, Jean-Pierre Talpin
- article
- 6th International Symposium on Static Analysis (SAS'99), Sep 1999, Venice, Italy. pp.51-68
- Accès au texte intégral et bibtex
-
Other publications
2016
- titre
- Using JavaScript Monitoring to Prevent Device Fingerprinting
- auteur
- Nataliia Bielova, Frédéric Besson, Thomas Jensen
- article
- 2016
- Accès au texte intégral et bibtex
-
2006
- titre
- A Formal Model of Access Control for Mobile Interactive Devices
- auteur
- Frédéric Besson, Guillaume Dufay, Thomas Jensen
- article
- 2006
- Accès au texte intégral et bibtex
-
Reports
2014
- titre
- Enforcing Browser Anonymity with Quantitative Information Flow
- auteur
- Frédéric Besson, Nataliia Bielova, Thomas Jensen
- article
- [Research Report] RR-8532, INRIA. 2014
- Accès au texte intégral et bibtex
-
2009
- titre
- Computing the Least Fix-point Semantics of Definite Logic Programs Using BDDs
- auteur
- Frédéric Besson, Thomas Jensen, Tiphaine Turpin
- article
- [Research Report] PI 1939, 2009, pp.25
- Accès au texte intégral et bibtex
-
2008
- titre
- Computing stack maps with interfaces
- auteur
- Frédéric Besson, Thomas Jensen, Tiphaine Turpin
- article
- [Research Report] PI 1879, 2008, pp.39
- Accès au texte intégral et bibtex
-
2007
- titre
- Result certification for relational program analysis
- auteur
- Frédéric Besson, Thomas Jensen, David Pichardie, Tiphaine Turpin
- article
- [Research Report] RR-6333, INRIA. 2007, pp.32
- Accès au texte intégral et bibtex
-
2005
- titre
- A PCC Architecture based on Certified Abstract Interpretation
- auteur
- Frédéric Besson, Thomas Jensen, David Pichardie
- article
- [Research Report] PI 1764, 2005, pp.35
- Accès au texte intégral et bibtex
-
- titre
- A PCC Architecture based on Certified Abstract Interpretation
- auteur
- Frédéric Besson, Thomas Jensen, David Pichardie
- article
- [Research Report] RR-5751, INRIA. 2005, pp.35
- Accès au texte intégral et bibtex
-