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 | 117 | 2001 |
Fast reflexive arithmetic tactics the linear case and beyond F Besson Types for Proofs and Programs: International Workshop, TYPES 2006 …, 2007 | 94 | 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 Static Analysis: 6th International Symposium, SAS’99 Venice, Italy …, 1999 | 71 | 1999 |
Sawja: Static Analysis Workshop for Java. L Hubert, N Barré, F Besson, D Demange, TP Jensen, V Monfort, ... FoVeOOS 6528, 92-106, 2010 | 44 | 2010 |
Hybrid information flow monitoring against web tracking F Besson, N Bielova, T Jensen 2013 IEEE 26th Computer Security Foundations Symposium, 240-254, 2013 | 41 | 2013 |
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 | 38 | 2002 |
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 | 35 | 2004 |
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 | 34 | 2014 |
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 | 33 | 2011 |
Modular SMT proofs for fast reflexive checking inside Coq F Besson, PE Cornilleau, D Pichardie Certified Programs and Proofs, 151-166, 2011 | 33 | 2011 |
Certified Result Checking for Polyhedral Analysis of Bytecode Programs. F Besson, TP Jensen, D Pichardie, T Turpin TGC 6084, 253-267, 2010 | 31 | 2010 |
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 | 28 | 2017 |
Certified static analysis by abstract interpretation F Besson, D Cachera, T Jensen, D Pichardie Foundations of Security Analysis and Design V: FOSAD 2007/2008/2009 Tutorial …, 2009 | 27 | 2009 |
Modular class analysis with datalog F Besson, T Jensen SAS, 19-36, 2003 | 27 | 2003 |
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 | 24 | 2006 |
A Concrete Memory Model for CompCert F Besson, S Blazy, P Wilke Interactive Theorem Proving (ITP 2105) 9236, 67-83, 2015 | 23 | 2015 |
Result certification for relational program analysis F Besson, T Jensen, D Pichardie, T Turpin INRIA, 2007 | 23 | 2007 |
Small witnesses for abstract interpretation-based proofs F Besson, T Jensen, T Turpin Programming Languages and Systems: 16th European Symposium on Programming …, 2007 | 20 | 2007 |
Information-flow preservation in compiler optimisations F Besson, A Dang, T Jensen 2019 IEEE 32nd Computer Security Foundations Symposium (CSF), 230-23012, 2019 | 16 | 2019 |