Adresse : Inria
Campus de Beaulieu
35042 RENNES Cedex - France
Email : frederic.besson@inria.fr 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 - Drafts
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.
Modular SMT Proofs for Fast Reflexive Checking inside Coq with P-E. Cornilleau and D. Pichardie.
In Certified Programs and Proofs (CPP'11), LNCS, © Springer 2011. To appear.
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 T.de 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.
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
A Coq proof that Agesen's Cartesian Product is more precise than ooCFA.
read browse download