Adresse : Irisa/Inria
Campus de Beaulieu
35042 RENNES Cedex - France
Email : frederic.besson@inria.fr
Tel : (+33|0) 2 99 84 72 25
I am researcher in the Epicure team of the Inria Rennes - Bretagne Atlantique research centre.
- Publications - Software - Proofs
End-to-end Mechanized Proof of an eBPF Virtual Machine for Micro-controllers In Computer Aided Verification (CAV), LNCS 13372, Springer 2022.
Itauto: an Extensible Intuitionistic SAT Solver In Interactive Theorem Proving (ITP), LIPIcs 2021.
Information-Flow Preservation in Compiler Optimisations with A. Dang and T. Jensen
In Computer Security Foundations Symposium (CSF), IEEE 2019.
Compiling Sandboxes:Formally Verified Software Fault Isolation with S. Blazy, A. Dang, T. Jensen and P. Wilke
In European Symposium on Programming (ESOP), LNCS 11423, Springer 2019.
Modular Software Fault Isolation as Abstract Interpretation with T. Jensen and J. Lepiller
In Static Analysis Symposium (SAS), LNCS 11002, Springer 2018.
CompCertS: A Memory-Aware Verified C Compiler using Pointer as Integer Semantics with S. Blazy and P. Wilke
In Interactive Theorem Proving (ITP), LNCS 10499, Springer 2017.
Hybrid Monitoring of Attacker Knowledge with N. Bielova and T. Jensen
In Computer Security Foundations Symposium (CSF), IEEE 2016.
A Concrete Memory Model for CompCert with S. Blazy and P. Wilke
In Interactive Theorem Proving (ITP), LNCS 9236, Springer 2015.
A Precise and Abstract Memory Model for C using Symbolic Values with S. Blazy and P. Wilke.
In Asian Symposium on Programming Languages and Systems (APLAS), LNCS 8858, Springer 2014.
Browser Randomisation against Fingerprinting: a Quantitative Information Flow Approach with N. Bielova and T. Jensen.
In Nordic Conference on Secure IT Systems (NordSec), LNCS 8788, Springer 2014.
SawjaCard: a static analysis tool for certifying Java Card applications with T. Jensen and P. Vittet.
In Static Analysis Symposium (SAS), LNCS 8723, Springer 2014.
Hybrid Information Flow Monitoring Against Web Tracking with N. Bielova and T. Jensen.
In Computer Security Foundations Symposium (CSF), pages 240-254, IEEE 2013.
Result Certification of Static Program Analysers with Automated Theorem Provers with P-E. Cornilleau and T. Jensen.
In Verified Software: Theories, Tools and Experiments (VSTTE), LNCS 8164, pages 304-325, Springer 2013.
Modular SMT Proofs for Fast Reflexive Checking inside Coq with P-E. Cornilleau and D. Pichardie.
In Certified Programs and Proofs (CPP), LNCS 7086, pages 151-166, Springer 2011.
Sawja: Static Analysis Workshop for Java with L. Hubert, N. Barré, D. Demange, T. Jensen, V. Monfort, D. Pichardie, T. Turpin.
In Formal Verification of Object-Oriented Software (FoVeOOS). LNCS 6528, pages 92-106, Springer 2011.
Certified Result Checking for Polyhedral Analysis of Bytecode Programs with T. Jensen, D. Pichardie and T. Turpin.
In Trustworthy Global Computing 2010 (TGC), LNCS 6084, pages 253-267, Springer 2010.
Computing Stack Maps with Interfaces with T. Jensen and T. Turpin.
In 22nd European Conference on Object Oriented Programming (ECOOP), LNCS 5142, pages 642-66, Springer 2008.
Small Witnesses for Abstract Interpretation-based Proofs with T. Jensen and T. Turpin.
In 16th European Symposium on Programming (ESOP), LNCS 4421, pages 268-283, Springer 2007.
Fast Reflexive Arithmetic Tactics: the linear case and beyond
In Types for Proofs and Programs (Types), LNCS 4502, pages 48-62, Springer 2007.
A Formal Model of Access Control for Mobile Interactive Devices with G. Dufay and T. Jensen.
In 11th European Symposium on Research in Computer Security (ESORICS), LNCS 4189, pages 110-126, Springer 2006.
From Stack Inspection to Access Control: A Security Analysis for Libraries with Tomasz Blanc, Cédric Fournet and Andrew D. Gordon.
In 17th IEEE Computer Security Foundations Workshop (CSFW), pages 61-75. IEEE Computer Society, 2004.
Modular class analysis with Datalog with T.Jensen.
In 10th Static Analysis Symposium (SAS). LNCS 2694, pages 19 - 36, Springer 2003.
Secure calling contexts for stack inspection with T.de Grenier de Latour and T.Jensen.
In 4th Conference on Principles and Practice of Declarative Programming (PPDP), pages 76-87, ACM Press.
Polyhedral analysis for synchronous languages with T.Jensen and J-P Talpin.
In 6th Static Analysis Symposium (SAS), LNCS 1684, pages 51-68, Springer 1999.
CompCertS: A Memory-Aware Verified C Compiler Using a Pointer as Integer Semantics with S. Blazy and P. Wilke. J. Autom. Reasoning 63(2): 369-392 (2019).
A Verified CompCert Front-End for a Memory Model supporting Pointer Arithmetic and Uninitialised Data with S. Blazy and P. Wilke.
J. Autom. Reasoning 62(4): 433-480 (2019).
Verifying resource access control on mobile interactive devices with G. Dufay, T. Jensen and D. Pichardie.
Journal of Computer Security 18(6):971-998 2010.
Proof-carrying code from Certified Abstract Interpretation and Fixpoint Compression with T. Jensen and D. Pichardie.
Theoretical Computer Science 364(3):273-291. Elsevier.
Interfaces for Stack Inspection with T.de Grenier de Latour and T.Jensen.
Journal of Functional Programming 15(2):179-217 2005.
Model checking security properties of control flow graphs with T.Jensen, D.Le Métayer and T.Thorn.
Journal of Computer Security 9:3:217-250 2001.
Securing Compilation Against Memory Probing with A. Dang and T. Jensen. In 13th Workshop on Programming Languages and Analysis for Security (PLAS). ACM 2018.
ppsimpl: a reflexive Coq tactic for canonising goals
In Third International Workshop on Coq for Programming Languages (CoqPL'17).
Walking through the Forest: Fast EUF Proof-Checking Algorithms with P-E. Cornilleau and R. Saillard.
In Second Workshop on Proof eXchange for Theorem Proving (PxTP'12), CEUR-WS 878, pages 58-64.
A Nelson-Oppen based Proof System using Theory Specific Proof Systems with P-E. Cornilleau and D. Pichardie.
In First Workshop on Proof eXchange for Theorem Proving (PxTP 2011).
On using an inexact floating-point LP solver for deciding linear arithmetic in an SMT solver
In SMT Workshop 2010.
CPA beats oo-CFA
In 11th Workshop on Formal Techniques for Java-like Programs (FTfJP'09), ACM 2009.
A PCC Architecture based on Certified Abstract Interpretation with T. Jensen and D. Pichardie.
In 1st International Workshop on Emerging Applications of Abstract Interpretation (EAAI). ENTCS, Springer 2006.
A PCC Architecture based on Certified Abstract Interpretation with T. Jensen and D. Pichardie.
Inria Research Report, RR 5751.
Résolution modulaire d'analyses de programmes: application à la sécurité logicielle
Thèse de doctorat. Université de Rennes I, Dec 2002.
itauto is a Coq tactic for (intuitionistic) propositional logic.
(Like intuition is can be parametrised by a leaf tactic.).
git clone https://gitlab.inria.fr/fbesson/itauto.git
A Coq proof that Agesen's Cartesian Product is more precise than ooCFA.
read browse download