Model checking security properties of control flow graphs F Besson, T Jensen, D Le Métayer, T Thorn Journal of computer security 9 (3), 217-250, 2001 | 115 | 2001 |
Fast reflexive arithmetic tactics the linear case and beyond F Besson Types for Proofs and Programs: International Workshop, TYPES 2006 …, 2007 | 106 | 2007 |
Proof-carrying code from certified abstract interpretation and fixpoint compression F Besson, T Jensen, D Pichardie Theoretical Computer Science 364 (3), 273-291, 2006 | 81 | 2006 |
Polyhedral analysis for synchronous languages F Besson, T Jensen, JP Talpin International Static Analysis Symposium, 51-68, 1999 | 71 | 1999 |
Hybrid information flow monitoring against web tracking F Besson, N Bielova, T Jensen 2013 IEEE 26th Computer Security Foundations Symposium, 240-254, 2013 | 47 | 2013 |
Sawja: Static analysis workshop for java L Hubert, N Barré, F Besson, D Demange, T Jensen, V Monfort, ... International Conference on Formal Verification of Object-Oriented Software …, 2010 | 43 | 2010 |
A Precise and Abstract Memory Model for C Using Symbolic Values F Besson, S Blazy, P Wilke Programming Languages and Systems - 12th Asian Symposium 8858, 449-468, 2014 | 39 | 2014 |
CompCertS: A Memory-Aware Verified C Compiler using Pointer as Integer Semantics F Besson, S Blazy, P Wilke Interactive Theorem Proving (ITP 2107) 10499, 2017 | 37 | 2017 |
Secure calling contexts for stack inspection F Besson, T de Grenier de Latour, T Jensen Proceedings of the 4th ACM SIGPLAN international conference on Principles …, 2002 | 37 | 2002 |
A flexible proof format for SMT: A proposal F Besson, P Fontaine, L Théry First International Workshop on Proof eXchange for Theorem Proving-PxTP 2011, 2011 | 35 | 2011 |
Modular SMT proofs for fast reflexive checking inside Coq F Besson, PE Cornilleau, D Pichardie Certified Programs and Proofs, 151-166, 2011 | 34 | 2011 |
From stack inspection to access control: A security analysis for libraries F Besson, T Blanc, C Fournet, AD Gordon Proceedings. 17th IEEE Computer Security Foundations Workshop, 2004., 61-75, 2004 | 33 | 2004 |
A Concrete Memory Model for CompCert F Besson, S Blazy, P Wilke Interactive Theorem Proving (ITP 2105) 9236, 67-83, 2015 | 32 | 2015 |
Certified result checking for polyhedral analysis of bytecode programs F Besson, T Jensen, D Pichardie, T Turpin International Symposium on Trustworthy Global Computing, 253-267, 2010 | 30 | 2010 |
Modular Class Analysis with DATALOG F Besson, T Jensen International Static Analysis Symposium, 19-36, 2003 | 28 | 2003 |
Certified static analysis by abstract interpretation F Besson, D Cachera, T Jensen, D Pichardie International School on Foundations of Security Analysis and Design, 223-257, 2007 | 25 | 2007 |
Result certification for relational program analysis F Besson, T Jensen, D Pichardie, T Turpin INRIA, 2007 | 24 | 2007 |
A formal model of access control for mobile interactive devices F Besson, G Dufay, T Jensen Computer Security–ESORICS 2006: 11th European Symposium on Research in …, 2006 | 23 | 2006 |
Information-flow preservation in compiler optimisations F Besson, A Dang, T Jensen 2019 IEEE 32nd Computer Security Foundations Symposium (CSF), 230-23012, 2019 | 22 | 2019 |
Small witnesses for abstract interpretation-based proofs F Besson, T Jensen, T Turpin European Symposium on Programming, 268-283, 2007 | 21 | 2007 |