Frédéric Besson, Sandrine Blazy, Pierre Wilke. CompCertS: A Memory-Aware Verified C Compiler using a Pointer as Integer Semantics. Journal of Automated Reasoning, Springer Verlag, 2019, 63 (2), pp.369-392. ⟨10.1007/s10817-018-9496-y⟩. ⟨hal-02401182⟩

Frédéric Besson, Sandrine Blazy, Pierre Wilke. A Verified CompCert Front-End for a Memory Model Supporting Pointer Arithmetic and Uninitialised Data. Journal of Automated Reasoning, Springer Verlag, 2019, 62 (4), pp.433-480. ⟨10.1007/s10817-017-9439-z⟩. ⟨hal-01656895⟩

Frédéric Besson, Guillaume Dufaye, Thomas Jensen, David Pichardie. Verifying Resource Access Control on Mobile Interactive Devices. Journal of Computer Security, IOS Press, 2010, 18 (6), pp.971-998. ⟨inria-00537821⟩

Frédéric Besson, Sandrine Blazy, Alexandre Dang, Thomas Jensen, Pierre Wilke. Compiling Sandboxes: Formally Verified Software Fault Isolation. ESOP 2019 - 28th European Symposium on Programming, Apr 2019, Prague, Czech Republic. pp.499-524, ⟨10.1007/978-3-030-17184-1_18⟩. ⟨hal-02316189⟩

Frédéric Besson, Alexandre Dang, Thomas Jensen. Information-Flow Preservation in Compiler Optimisations. CSF 2019 - 32nd IEEE Computer Security Foundations Symposium, Jun 2019, Hoboken, United States. pp.1-13. ⟨hal-02180303⟩

Frédéric Besson, Thomas Jensen, Julien Lepiller. Modular Software Fault Isolation as Abstract Interpretation. SAS 2018 - 25th International Static Analysis Symposium, Aug 2018, Freiburg, Germany. pp.166-186, ⟨10.1007/978-3-319-99725-4_12⟩. ⟨hal-01894116⟩

Frédéric Besson, Alexandre Dang, Thomas Jensen. Securing Compilation Against Memory Probing. PLAS '18 - 13th Workshop on Programming Languages and Analysis for Security, Oct 2018, Toronto, Canada. pp.29-40, ⟨10.1145/3264820.3264822⟩. ⟨hal-01901765⟩

Florent Saudel, Sandrine Blazy, Frédéric Besson. Confusion de Type en C++: État de l'Art et Difficultés de Détection. 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. ⟨hal-01656979⟩

Frédéric Besson, Sandrine Blazy, Pierre Wilke. CompCertS: A Memory-Aware Verified C Compiler using Pointer as Integer Semantics. ITP 2017 - 8th International Conference on Interactive Theorem Proving, Sep 2017, Brasilia, Brazil. pp.81-97, ⟨10.1007/978-3-319-66107-0_6⟩. ⟨hal-01656875⟩

Frédéric Besson, Nataliia Bielova, Thomas Jensen. Hybrid Monitoring of Attacker Knowledge. 29th IEEE Computer Security Foundations Symposium, 2016, Lisboa, Portugal. ⟨hal-01310572⟩

Frédéric Besson, Sandrine Blazy, Pierre Wilke. A Concrete Memory Model for CompCert. ITP 2015 : 6th International Conference on Interactive Theorem Proving, Aug 2015, Nanjing, China. pp.67-83, ⟨10.1007/978-3-319-22102-1_5⟩. ⟨hal-01194549⟩

Frédéric Besson, Thomas Jensen, Pierre Vittet. SawjaCard: A Static Analysis Tool for Certifying Java Card Applications. 21st International Static Analysis Symposium (SAS 2014), 2014, Munich, Germany. pp.51 - 67, ⟨10.1007/978-3-319-10936-7_4⟩. ⟨hal-01093327⟩

Frédéric Besson, Nataliia Bielova, Thomas Jensen. Browser Randomisation against Fingerprinting: A Quantitative Information Flow Approach. Nordic Conference on Secure IT Systems (NordSec 2014), Oct 2014, Tromsø, Norway. ⟨10.1007/978-3-319-11599-3_11⟩. ⟨hal-01081037⟩

Frédéric Besson, Sandrine Blazy, Pierre Wilke. A Precise and Abstract Memory Model for C Using Symbolic Values. 12th Asian Symposium on Programming Languages and Systems (APLAS 2014), 2014, Singapore, Singapore. pp.449 - 468, ⟨10.1007/978-3-319-12736-1_24⟩. ⟨hal-01093312⟩

Frédéric Besson, Pierre-Emmanuel Cornilleau, Thomas Jensen. Result Certification of Static Program Analysers with Automated Theorem Provers. VSTTE 2013 - Fifth Working Conference on Verified Software: Theories, Tools and Experiments, 2013, Atherthon, United States. ⟨hal-00924167⟩

Frédéric Besson, Nataliia Bielova, Thomas Jensen. Hybrid Information Flow Monitoring Against Web Tracking. CSF - 2013 IEEE 26th Computer Security Foundations Symposium, 2013, New Orleans, United States. ⟨10.1109/CSF.2013.23⟩. ⟨hal-00924138⟩

Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie. Modular SMT Proofs for Fast Reflexive Checking inside Coq. First International Conference on Certified Programs and Proofs, 2011, Kenting, Taiwan. ⟨hal-00646960⟩

Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie. A Nelson-Oppen based Proof System using Theory Specific Proof Systems. First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland. ⟨hal-00677193⟩

Frédéric Besson, Pascal Fontaine, Laurent Théry. A Flexible Proof Format for SMT: a Proposal. First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland. ⟨hal-00642544⟩

Frédéric Besson, Thomas Jensen, David Pichardie, Tiphaine Turpin. Certified Result Checking for Polyhedral Analysis of Bytecode Programs. The 5th International Symposium on Trustworthy Global Computing (TGC), 2010, Munich, Germany. ⟨inria-00537816⟩

Laurent Hubert, Nicolas Barré, Frédéric Besson, Delphine Demange, Thomas Jensen, et al.. Sawja: Static Analysis Workshop for Java. The International Conference on Formal Verification of Object-Oriented Software, Beckert, Bernhard and Marché, Claude, 2010, Paris, France. pp.253--267. ⟨inria-00504047⟩

Frédéric Besson. On using an inexact floating-point LP solver for deciding linear arithmetic in an SMT solver. 8th International Workshop on Satisfiability Modulo Theories, 2010, Edinburgh, United Kingdom. ⟨inria-00517308⟩

Frédéric Besson. CPA beats oo-CFA. FTfJP '09 - Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs, 2009, Genova, Italy. ⟨10.1145/1557898.1557905⟩. ⟨hal-00780389⟩

Frédéric Besson, David Cachera, Thomas Jensen, David Pichardie. Certified Static Analysis by Abstract Interpretation. Foundations of Security Analysis and Design V (FOSAD), 2009, Bertinoro, Italy. pp.223-257. ⟨inria-00538753⟩

Frédéric Besson, Thomas Jensen, Tiphaine Turpin. Computing stack maps with interfaces. ECOOP'08, 2008, Paphos, Cyprus. ⟨inria-00332526⟩

Frédéric Besson, Thomas Jensen, Jean-Pierre Talpin. Polyhedral Analysis for Synchronous Languages. 6th International Symposium on Static Analysis (SAS'99), Sep 1999, Venice, Italy. pp.51-68. ⟨hal-00544493⟩

Nataliia Bielova, Frédéric Besson, Thomas Jensen. Using JavaScript Monitoring to Prevent Device Fingerprinting. 2016. ⟨hal-01353997⟩

Frédéric Besson, Guillaume Dufay, Thomas Jensen. A Formal Model of Access Control for Mobile Interactive Devices. 2006. ⟨inria-00083453⟩

Frédéric Besson, Nataliia Bielova, Thomas Jensen. Enforcing Browser Anonymity with Quantitative Information Flow. [Research Report] RR-8532, INRIA. 2014. ⟨hal-00984654v2⟩

Frédéric Besson, Thomas Jensen, Tiphaine Turpin. Computing the Least Fix-point Semantics of Definite Logic Programs Using BDDs. [Research Report] PI 1939, 2009, pp.25. ⟨inria-00433820v2⟩

Frédéric Besson, Thomas Jensen, Tiphaine Turpin. Computing stack maps with interfaces. [Research Report] PI 1879, 2008, pp.39. ⟨inria-00200724v2⟩

Frédéric Besson, Thomas Jensen, David Pichardie, Tiphaine Turpin. Result certification for relational program analysis. [Research Report] RR-6333, INRIA. 2007, pp.32. ⟨inria-00166930v4⟩

Frédéric Besson, Thomas Jensen, David Pichardie. A PCC Architecture based on Certified Abstract Interpretation. [Research Report] PI 1764, 2005, pp.35. ⟨inria-00000866⟩

Frédéric Besson, Thomas Jensen, David Pichardie. A PCC Architecture based on Certified Abstract Interpretation. [Research Report] RR-5751, INRIA. 2005, pp.35. ⟨inria-00070268⟩

Pierre Nicolle, C. Perrin, V. Andreassian, B. Augeard, Frédéric Besson, et al.. Prévoir les étiages : que peut-on attendre des modèles hydrologiques ?. France. 2015, pp.24. ⟨hal-02603376⟩