Publications of Thomas Jensen

Load the BibTeX file

Proceedings

  1. M. Huisman, T. Jensen (eds.). J. Logic and Algebraic Programming. Special issue on Formal Methods for Smart Cards, vol. 58(1-2). Elsevier, 2004.
  2. Isabelle Attali, Thomas Jensen (eds.). Smart Card Programming and Security (e-Smart 2001). Springer LNCS vol. 2140, September 2001.
  3. I. Attali, T. Jensen (eds.). Proceedings of the International Workshop on Java Card (Java Card 2000). Inria, Cannes, France, September 2000.

Academic Journals

  1. David Cachera, Thomas Jensen, Arnaud Jobin, Florent Kirchner. Inference of polynomial invariants for imperative programs: a farewell to Gröbner bases. Science of Computer Programming, To appear, 2014. download
  2. Jan Midtgaard, Thomas Jensen. Control-Flow Analysis by Abstract Interpretation. Information and Computation, 2012.
  3. Jan Midtgaard, Thomas Jensen. Control Flow Analysis of Function Calls and Returns by Abstract Interpretation. Information and Computation, 211:49-76, 2012.
  4. Thomas Jensen, Florent Kirchner, David Pichardie. Secure the Clones: Static Enforcement of Policies for Secure Object Copying. Logical Methods in Computer Science (LMCS), 8(2), 2012.
  5. David Cachera, Thomas Jensen, Arnaud Jobin, Pascal Sotin. Long-Run Cost Analysis by Approximation of Linear Operators over Dioids. Mathematical Structures in Computer Science, 20(4):589-624, 2010.
  6. Frédéric Besson, Thomas Jensen, Guillaume Dufay, David Pichardie. Verifying Resource Access Control on Mobile Interactive Devices. Journal of Computer Security, 18(6):971-998, 2010.
  7. Frédéric Besson, Thomas Jensen, David Pichardie. Proof-Carrying Code from Certified Abstract Interpretation to Fixpoint Compression. Theoretical Computer Science, 364(3):273-291, 2006.
  8. F. Besson, T. de Grenier de Latour, T. Jensen. Interfaces for stack inspection. Journal of Functional Programming, 15(2):179-217, 2005. download
  9. David Cachera, Thomas Jensen, David Pichardie, Vlad Rusu. Extracting a Data Flow Analyser in Constructive Logic. Theoretical Computer Science, 2005.
  10. M. Eluard, T. Jensen. Vérification du contrôle d'accès dans des cartes à puce multi-application. Technique et Science Informatiques, 23(3):323-358, 2004.
  11. T. Jensen, J.-L. Lanet. Modélisation et vérification dans les cartes à puce. Revue d'électricité et de l'électronique, 6/7:89-94, 2004.
  12. A. Banerjee, T. Jensen. Control-flow analysis with rank-2 intersection types. Mathematical Structures in Computer Science, 13(1):87-124, 2003.
  13. F. Spoto, T. Jensen. Class Analyses as Abstract Interpretations of Trace Semantics. ACM Transactions on Programming Languages and Systems (TOPLAS), 25(5):578-630, 2003.
  14. E. Denney, T. Jensen. Correctness of Java Card method lookup via logical relations. Theoretical Computer Science, 283:305-331, 2002.
  15. F. Besson, T. Jensen, D. Le Métayer, T. Thorn. Model ckecking security properties of control flow graphs. Journal of Computer Security, 9:217-250, 2001. download
  16. T. Jensen. Disjunctive Program Analysis for Algebraic Data Types. ACM Transactions on Programming Languages and Systems, 19(5):752-804, 1997. ps

Book Chapters

  1. T. Jensen. Types in program analysis. In The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, Torben Mogensen, David Schmidt, I. Hal Sudborough (eds.), pp. 204-222, Lecture Notes in Computer Science 2566, Springer-Verlag, 2002.

International Conferences

  1. Frédéric Besson, Nataliia Bielova, Thomas Jensen. Hybrid Information Flow Monitoring Against Web Tracking. In CSF - 2013 IEEE 26th Computer Security Foundations Symposium, New Orleans, United States, 2013. download
  2. Frédéric Besson, Pierre-Emmanuel Cornilleau, Thomas Jensen. Result Certification of Static Program Analysers with Automated Theorem Provers. In VSTTE 2013 - Fifth Working Conference on Verified Software: Theories, Tools and Experiments, Atherthon, United States, 2013. download
  3. David Cachera, Thomas Jensen, Arnaud Jobin, Florent Kirchner. Inference of polynomial invariants for imperative programs: a farewell to Gröbner bases. In SAS - 19th International Static Analysis Symposium - 2012, Projet Région Bretagne CertLogs, Deauville, France, September 2012. download
  4. Thomas Jensen, Florent Kirchner, David Pichardie. Secure the Clones: Static Enforcement of Policies for Secure Object Copying. In Proc. of 20th European Symposium on Programming (ESOP 2011), Lecture Notes in Computer Science, Volume 6602, Pages 317-337, 2011.
  5. Delphine Demange, Thomas Jensen, David Pichardie. A Provably Correct Stackless Intermediate Representation for Java Bytecode. In 8th Asian Symposium on Programming Languages and Systems (APLAS), Lecture Notes in Computer Science, Volume 6461, 2010.
  6. Frédéric Besson, Thomas Jensen, David Pichardie, Tiphaine Turpin. Certified Result Checking for Polyhedral Analysis of Bytecode Programs. In Proc.\ of the 5th International Symposium on Trustworthy Global Computing (TGC 2010), Lecture Notes in Computer Science, Volume 6084, Pages 253-267, 2010.
  7. Laurent Hubert, Nicolas Barré, Frédéric Besson, Delphine Demange, Thomas Jensen, Vincent Monfort, David Pichardie, Tiphaine Turpin. Sawja: Static Analysis Workshop for Java. In 1st International Conference on Formal Verification of Object-Oriented Software (FoVeOOS), Lecture Notes in Computer Science, 2010.
  8. Laurent Hubert, Thomas Jensen, Vincent Monfort, David Pichardie. Enforcing Secure Object Initialization in Java. In 15th European Symposium on Research in Computer Security (ESORICS), Lecture Notes in Computer Science, Volume 6345, Pages 101-115, 2010.
  9. Jan Midtgaard, Thomas Jensen. Control-flow analysis of function calls and returns by abstract interpretation. In Proceedings of the 14th ACM international conference on Functional programming, Pages 287-298, 2009.
  10. Frédéric Besson, Thomas Jensen, T. Turpin. Computing stack maps with interfaces. In Proc. of the 22nd European Conference on Object-Oriented Programming (ECOOP 2008), LNCS, Volume 5142, Pages 642-666, 2008.
  11. J. Midtgaard, Thomas Jensen. A Calculational Approach to Control-Flow Analysis by Abstract Interpretation. In Static Analysis, 15th International Symposium, SAS 2008, Lectures Notes in Computer Science, Volume 5079, Pages 347-362, 2008.
  12. B. Boyer, Thomas Genet, Thomas Jensen. Certifying a Tree Automata Completion Checker. In 4th International Joint Conference, IJCAR 2008, Lectures Notes in Computer Science, Volume 5195, Pages 347-362, 2008.
  13. David Cachera, Thomas Jensen, Arnaud Jobin, Pascal Sotin. Long-Run Cost Analysis by Approximation of Linear Operators over Dioids. In Algebraic Methodology and Software Technology, 12th International Conference, AMAST 2008, Lectures Notes in Computer Science, Volume 5140, Pages 122-138, 2008.
  14. Laurent Hubert, Thomas Jensen, David Pichardie. Semantic foundations and inference of non-null annotations. In Proc.\ of the 10th International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS'08), Lecture Notes in Computer Science, Volume 5051, Pages 132-149, 2008.
  15. Gilles Barthe, Pierre Crégut, Benjamin Grégoire, Thomas Jensen, David Pichardie. The MOBIUS Proof Carrying Code infrastructure. In Proc.\ of the 6th International Symposium on Formal Methods for Components and Objects (FMCO'07), Lecture Notes in Computer Science, Volume 5382, Pages 1-24, 2008.
  16. Y. Boichut, T. Genet, T. Jensen, L. Leroux. Rewriting Approximations for Fast Prototyping of Static Analyzers. In RTA, LNCS, Volume 4533, Pages 48-62, 2007.
  17. F. Besson, T. Jensen, T. Turpin. Small Witnesses for Abstract Interpretation-Based proofs. In Proc. of 16th European Symposium on Programming (ESOP'07), LNCS, Volume 4421, Pages 268-283, 2007.
  18. F. Besson, T. Jensen, D. Pichardie. A PCC Architecture based on Certified Abstract Interpretation. In Proc. of 1st International Workshop on Emerging Applications of Abstract Interpretation (EAAI'06), ENTCS, 2006. download
  19. Frédéric Besson, Guillaume Dufay, Thomas Jensen. A Formal Model of Access Control for Mobile Interactive Devices. In 11th European Symposium On Research In Computer Security (ESORICS'06), Lecture Notes in Computer Science, Volume 4189, 2006. download
  20. Pascal Sotin, David Cachera, Thomas Jensen. Quantitative Static Analysis over semirings: analysing cache behaviour for Java Card. In 4th International Workshop on Quantitative Aspects of Programming Languages (QAPL 2006), Electronic Notes in Theoretical Computer Science, Volume 164, Pages 153-167, 2006.
  21. G. Le Guernic, A. Banerjee, T. Jensen, D. Schmidt. Automata-based Confidentiality Monitoring. In Proceedings of the Annual Asian Computing Science Conference, Lecture Notes in Computer Science, To appear, Volume 4435, 2006. pdf
  22. Gurvan Le Guernic, Anindya Banerjee, Thomas Jensen, David Schmidt. Automaton-based Confidentiality Monitoring. In 11th Annual Asian Computing Science Conference (ASIAN'06), Lecture Notes in Computer Science, to appear, Volume 4435, Tokyo, Japan, December 2006.
  23. David Cachera, Thomas Jensen, David Pichardie, Gerardo Schneider. Certified Memory Usage Analysis. In Proc\. of 13th International Symposium on Formal Methods (FM'05), Lecture Notes in Computer Science, 2005.
  24. David Cachera, Thomas Jensen, Pascal Sotin. Estimating Cache Misses with Semi-Modules and Quantitative Abstraction. In Proc. of IST-APPSEM II Workshop on Applied Semantics, 2005.
  25. G. Le Guernic, T. Jensen. Monitoring Information Flow. In Proceedings of the Workshop on Foundations of Computer Security, Andrei Sabelfeld (ed.), Pages 19-30, June 2005. pdf
  26. David Cachera, Thomas Jensen, David Pichardie, Vlad Rusu. Extracting a data flow analyser in constructive logic. In Proc. ESOP'04, Springer LNCS, Pages 385-400, 2004.
  27. Lionel van Aertryck, Thomas Jensen. UML-CASTING: Test synthesis from UML models using constraint resolution. In Proc. Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL'2003), J-M. Jézéquel (ed.), 2003.
  28. F. Besson, T. Jensen. Modular Class Analysis with DATALOG. In Proc. of 10th Static Analysis Symposium (SAS 2003), R. Cousot (ed.), Pages 19-36, 2003. download
  29. T. Genet, T. Jensen, V. Kodati, D. Pichardie. A Java Card CAP Converter in PVS. In Proceedings of the 2nd International Workshop on Compiler Optimization Meets Compiler Verification (COCV 2003), 2003. download
  30. F. Besson, Thomas de Grenier de Latour, T. Jensen. Secure calling contexts for stack inspection. In Proc. of 4th Int Conf. on Principles and Practice of Declarative Programming (PPDP 2002), Pages 76-87, 2002. download
  31. Marc Éluard, Thomas Jensen. Secure object flow analysis for Java Card. In Proc. of 5th Smart Card Research and Advanced Application Conference (Cardis'02), 2002.
  32. Thomas Jensen, Florimond Ployette, Olivier Ridoux. Iteration schemes for fixed point conputation. In Proc. of 4th Int workshop on Fixed Points in Computer Science (FICS'02), A. Ingolfsdottir, Z. Esik (eds.), Pages 69-76, 2002.
  33. T. Jensen, F. Spoto. Class analysis of object-oriented programs through abstract interpretation. In Proc. of Foundations of Software Science and Computation Structures (FoSSaCS'01), F. Honsell, M. Miculan (eds.), Pages 261-275, 2001.
  34. Igor Siveroni, Thomas Jensen, Marc Éluard. A Formal Specification of the Java Card Applet Firewall. In Nordic Workshop on Secure IT-Systems, Hanne Riis Nielson (ed.), November 2001.
  35. Marc Éluard, Thomas Jensen, Ewen Denney. An Operational Semantics of the Java Card Firewall. In Smart Card Programming and Security (e-Smart 2001, Isabelle Attali, Thomas Jensen (eds.), Volume Springer LNCS vol. 2140, September 2001.
  36. E. Denney, T. Jensen. Correctness of Java Card method lookup via logical relations. In Proc. of European Symp. on Programming (ESOP 2000), Lecture Notes in Computer Science, Pages 104-118, 2000.
  37. F. Besson, T. Jensen, J.P. Talpin. Polyhedral Analysis for Synchronous Languages. In International Static Analysis Symposium, SAS'99, Gilberto Filé (ed.), Lecture Notes in Computer Science, Volume 1694, September 1999.
  38. T. Jensen, D. Le Métayer, T. Thorn. Verification of control flow based security properties. In Proc.\ of the 20th IEEE Symp. on Security and Privacy, Pages 89-103, May 1999.
  39. T. Jensen. Inference of polymorphic and conditional strictness properties. In Proc. of 25th ACM Symposium on Principles of Programming Languages, Pages 209-221, 1998. ps
  40. T. Jensen, D. Le Métayer, T. Thorn. Security and Dynamic Class Loading in Java: A Formalisation. In Proceedings of the 1998 IEEE International Conference on Computer Languages, Pages 4-15, May 1998. ps

National Conferences

  1. J. Midtgaard, Thomas Jensen. A Calculational Approach to Control-Flow Analysis by Abstract Interpretation. In Proc. of the 15th Static Aanalysi Symposium, LNCS, Volume 5079, Pages 347-362, 2008.

Research Reports

  1. David Cachera, Thomas Jensen, Arnaud Jobin, Florent Kirchner. Fast inference of polynomial invariants for imperative programs. Research Report INRIA, No 0, May 2011. download
  2. Tiphaine Turpin, Frédéric Besson, Thomas Jensen. Computing the Least Fix-point Semantics of Logic Programs Using BDDs. Research Report INRIA, No 7107, 2009.
  3. Delphine Demange, Thomas Jensen, David Pichardie. A Provably Correct Stackless Intermediate Representation For Java Bytecode. Research Report INRIA, No 0, 2009. download
  4. David Cachera, Thomas Jensen, Pascal Sotin. Long-Run Cost Analysis by Approximation of Linear Operators over Dioids. Research Report INRIA, No 6338, 2007. download
  5. F. Besson, T. Jensen, D. Pichardie, T. Turpin. Result certification for relational program analysis. Research Report Inria, No 6333, September 2007. download
  6. F. Besson, T. Jensen, D. Pichardie. A PCC Architecture based on Certified Abstract Interpretation. Research Report INRIA, No 0, November 2005.
  7. T. Jensen, D. Le Métayer, T. Thorn. Verification of control flow based security policies. Research Report IRISA, No 1210, 1998. ps

Misc

  1. Fré Besson, David Cachera, Thomas Jensen, David Pichardie. Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures. pp. 223-257, 2009.
  2. E. Denney, P. Fradet, C. Goire, T. Jensen, D. Le Métayer. Procédé de vérification de transformateurs de codes pour un système embarqué, notamment sur une carte à puce. July 1999.

Thesis

  1. Thomas Jensen. Analyse statiques de programmes : fondements et applications. Habilitation à diriger des recherches Université de Rennes 1, December 1999.