Frédéric Besson

Adresse : Irisa/Inria
Campus de Beaulieu
35042 RENNES Cedex - France
Email : pgp key
Tel : (+33|0) 2 99 84 72 25

I am researcher in the Celtique team of the Inria Rennes - Bretagne Atlantique research centre.

- Publications - Software - Proofs


Hal Inria Google Scholar

In proceedings

Hybrid Monitoring of Attacker Knowledge with N. Bielova and T; Jensen
In Computer Security Foundations Symposium (CSF'16), IEEE 2016.

A Concrete Memory Model for CompCert with S. Blazy and P. Wilke
In Interactive Theorem Proving (ITP'15), 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'14), 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 2014), 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'14), LNCS 8723, Springer 2014.

Hybrid Information Flow Monitoring Against Web Tracking with N. Bielova and T. Jensen.
In Computer Security Foundations Symposium (CSF'13), 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'13), 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'11), 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'10). 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 (TGC2010), 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'08), 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'07), LNCS 4421, pages 268-283, Springer 2007.

Fast Reflexive Arithmetic Tactics: the linear case and beyond
In Types for Proofs and Programs (Types'06), 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'06), 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 2004), pages 61-75. IEEE Computer Society, 2004.

Modular class analysis with Datalog with T.Jensen.
In 10th Static Analysis Symposium (SAS'03). LNCS 2694, pages 19 - 36, Springer 2003.

Secure calling contexts for stack inspection with Grenier de Latour and T.Jensen.
In 4th Conference on Principles and Practice of Declarative Programming (PPDP'02), pages 76-87, ACM Press.

Polyhedral analysis for synchronous languages with T.Jensen and J-P Talpin.
In 6th Static Analysis Symposium (SAS'99), LNCS 1684, pages 51-68, Springer 1999.


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 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.


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'06). 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.


Micromega is a fast Coq reflexive tactic for linear (and bits of non-linear) arithmetic. (now part of Coq)
read browse

ppsimpl is a Coq tactic for pre-processing quantifier-free formula.
(In particular, it extends the scope of arithmetics decision procedures such as lia and omega.)
website git clone

itauto is a Coq tactic for (intuitionistic) propositional logic.
(It is similar to rtauto but can generate subgoals (much like intuition)).
git clone


A Coq proof that Agesen's Cartesian Product is more precise than ooCFA.
read browse download


Abstract arithmetisation of the heap
more info