BACK TO INDEX

Publications of Thomas Jensen

Books and proceedings

  1. M. Huisman and T. Jensen, editors. J. Logic and Algebraic Programming. Special issue on Formal Methods for Smart Cards, vol. 58(1-2), 2004. Elsevier. [bibtex-entry]


  2. Isabelle Attali and Thomas Jensen, editors. Smart Card Programming and Security (e-Smart 2001), September 2001. Springer LNCS vol. 2140. [bibtex-entry]


  3. I. Attali and T. Jensen, editors. Proceedings of the International Workshop on Java Card (Java Card 2000), Cannes, France, Septembre 2000. Inria. [bibtex-entry]


Thesis

  1. Thomas Jensen. Analyse statiques de programmes : fondements et applications. document d'habilitation à diriger des recherches, Université de Rennes 1, décembre 1999. [bibtex-entry]


Articles in journal or book chapters

  1. Frédéric Besson, Thomas Jensen, and David Pichardie. Proof-Carrying Code from Certified Abstract Interpretation to Fixpoint Compression. Theoretical Computer Science, 364(3):273-291, 2006. [bibtex-entry]


  2. F. Besson, T. de Grenier de Latour, and T. Jensen. Interfaces for stack inspection. Journal of Functional Programming, 15(2):179-217, 2005. [WWW] [Abstract] [bibtex-entry]


  3. David Cachera, Thomas Jensen, David Pichardie, and Vlad Rusu. Extracting a Data Flow Analyser in Constructive Logic. Theoretical Computer Science, 2005. [Abstract] [bibtex-entry]


  4. M. Eluard and 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. [bibtex-entry]


  5. T. Jensen and J.-L. Lanet. Modélisation et vérification dans les cartes à puce. Revue d'électricité et de l'électronique, 6/7:89-94, 2004. [bibtex-entry]


  6. A. Banerjee and T. Jensen. Control-flow analysis with rank-2 intersection types. Mathematical Structures in Computer Science, 13(1):87-124, 2003. [bibtex-entry]


  7. F. Spoto and T. Jensen. Class Analyses as Abstract Interpretations of Trace Semantics. ACM Transactions on Programming Languages and Systems (TOPLAS), 25(5):578-630, 2003. [bibtex-entry]


  8. T. Jensen. Types in program analysis. In Torben Mogensen, David Schmidt, and I. Hal Sudborough, editors, The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, Lecture Notes in Computer Science 2566, pages 204-222. Springer-Verlag, 2002. [bibtex-entry]


  9. E. Denney and T. Jensen. Correctness of Java Card method lookup via logical relations. Theoretical Computer Science, 283:305-331, 2002. [bibtex-entry]


  10. F. Besson, T. Jensen, D. Le Métayer, and T. Thorn. Model ckecking security properties of control flow graphs. Journal of Computer Security, 9:217-250, 2001. [WWW] [Abstract] [bibtex-entry]


  11. T. Jensen. Disjunctive Program Analysis for Algebraic Data Types. ACM Transactions on Programming Languages and Systems, 19(5):752-804, 1997. [WWW] [Abstract] [bibtex-entry]


Conference articles

  1. Frédéric Besson, Thomas Jensen, and Tiphaine Turpin. Small Witnesses for Abstract Interpretation-Based proofs. In Proc. of 16th European Symposium on Programming, volume 4421 of Lecture Notes in Computer Science, pages 268-283, 2007. Springer. [bibtex-entry]


  2. Y. Boichut, T. Genet, T. Jensen, and L. Leroux. Rewriting Approximations for Fast Prototyping of Static Analyzers. In RTA, volume 4533 of LNCS, pages 48-62, 2007. Springer Verlag. [bibtex-entry]


  3. Frédéric Besson, Guillaume Dufay, and Thomas Jensen. A Formal Model of Access Control for Mobile Interactive Devices. In 11th European Symposium On Research In Computer Security (ESORICS'06), volume 4189 of Lecture Notes in Computer Science, 2006. Springer. [WWW] [Abstract] [bibtex-entry]


  4. F. Besson, T. Jensen, and 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. Springer-Verlag. [WWW] [Abstract] [bibtex-entry]


  5. G. Le Guernic, A. Banerjee, T. Jensen, and D. Schmidt. Automata-based Confidentiality Monitoring. In Proceedings of the Annual Asian Computing Science Conference, volume 4435 of Lecture Notes in Computer Science, DEC 6--8 2006. Note: To appear. [PDF] [Abstract] [bibtex-entry]


  6. Gurvan Le Guernic, Anindya Banerjee, Thomas Jensen, and David Schmidt. Automaton-based Confidentiality Monitoring. In 11th Annual Asian Computing Science Conference (ASIAN'06), volume 4435 of Lecture Notes in Computer Science, Tokyo, Japan, December 2006. Note: To appear. [bibtex-entry]


  7. Pascal Sotin, David Cachera, and 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), volume 164 of Electronic Notes in Theoretical Computer Science, pages 153-167, 2006. Elsevier. [bibtex-entry]


  8. David Cachera, Thomas Jensen, David Pichardie, and Gerardo Schneider. Certified Memory Usage Analysis. In Proc of 13th International Symposium on Formal Methods (FM'05), Lecture Notes in Computer Science, 2005. Springer-Verlag. [Abstract] [bibtex-entry]


  9. David Cachera, Thomas Jensen, and Pascal Sotin. Estimating Cache Misses with Semi-Modules and Quantitative Abstraction. In Proc. of IST-APPSEM II Workshop on Applied Semantics, 2005. [bibtex-entry]


  10. G. Le Guernic and T. Jensen. Monitoring Information Flow. In Andrei Sabelfeld, editor, Proceedings of the 2005 Workshop on Foundations of Computer Security (FCS'05), pages 19-30, June 2005. DePaul University. Note: LICS'05 Affiliated Workshop. [Abstract] [bibtex-entry]


  11. G. Le Guernic and T. Jensen. Monitoring Information Flow. In Andrei Sabelfeld, editor, Proceedings of the Workshop on Foundations of Computer Security, pages 19-30, June 2005. DePaul University. [PDF] [Abstract] [bibtex-entry]


  12. David Cachera, Thomas Jensen, David Pichardie, and Vlad Rusu. Extracting a data flow analyser in constructive logic. In Proc. ESOP'04, number 2986 of Springer LNCS, pages 385 - 400, 2004. [bibtex-entry]


  13. F. Besson and T. Jensen. Modular Class Analysis with DATALOG. In R. Cousot, editor, Proc. of 10th Static Analysis Symposium (SAS 2003), pages 19-36, 2003. Springer LNCS vol. 2694. [WWW] [Abstract] [bibtex-entry]


  14. T. Genet, T. Jensen, V. Kodati, and 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. ENTCS 82(2). [WWW] Keyword(s): Java, Java Card, CAP Format, Compiler, Verification, Proof Assistant, PVS. [bibtex-entry]


  15. Lionel van Aertryck and Thomas Jensen. UML-CASTING: Test synthesis from UML models using constraint resolution. In J-M. Jézéquel, editor, Proc. Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL'2003), 2003. INRIA. [bibtex-entry]


  16. F. Besson, Thomas de Grenier de Latour, and 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. ACM Press. [WWW] [Abstract] [bibtex-entry]


  17. Thomas Jensen, Florimond Ployette, and Olivier Ridoux. Iteration schemes for fixed point conputation. In A. Ingolfsdottir and Z. Esik, editors, Proc. of 4th Int workshop on Fixed Points in Computer Science (FICS'02), pages 69-76, 2002. [bibtex-entry]


  18. Marc Éluard and Thomas Jensen. Secure object flow analysis for Java Card. In Proc. of 5th Smart Card Research and Advanced Application Conference (Cardis'02), 2002. IFIP/USENIX. [bibtex-entry]


  19. T. Jensen and F. Spoto. Class analysis of object-oriented programs through abstract interpretation. In F. Honsell and M. Miculan, editors, Proc. of Foundations of Software Science and Computation Structures (FoSSaCS'01), pages 261-275, 2001. Springer LNCS vol .2030. [bibtex-entry]


  20. Igor Siveroni, Thomas Jensen, and Marc Éluard. A Formal Specification of the Java Card Applet Firewall. In Hanne Riis Nielson, editor, Nordic Workshop on Secure IT-Systems, November 2001. [bibtex-entry]


  21. Marc Éluard, Thomas Jensen, and Ewen Denney. An Operational Semantics of the Java Card Firewall. In Isabelle Attali and Thomas Jensen, editors, Smart Card Programming and Security (e-Smart 2001, volume Springer LNCS vol. 2140, September 2001. [bibtex-entry]


  22. E. Denney and 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. Springer. [bibtex-entry]


  23. F. Besson, T. Jensen, and J.P. Talpin. Polyhedral Analysis for Synchronous Languages. In Gilberto Filé, editor, International Static Analysis Symposium, SAS'99, volume 1694 of Lecture Notes in Computer Science, September 1999. Springer-Verlag. Keyword(s): synchronous languages, abstract interpretation, reachability analysis, infinite state systems. [Abstract] [bibtex-entry]


  24. T. Jensen, D. Le Métayer, and T. Thorn. Verification of control flow based security properties. In Proc. of the 20th IEEE Symp. on Security and Privacy, pages 89-103, mai 1999. New York: IEEE Computer Society. [bibtex-entry]


  25. T. Jensen. Inference of polymorphic and conditional strictness properties. In Proc. of 25th ACM Symposium on Principles of Programming Languages, pages 209-221, 1998. ACM Press. [WWW] [Abstract] [bibtex-entry]


  26. T. Jensen, D. Le Métayer, and 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. New York: IEEE Computer Society. [WWW] [Abstract] [bibtex-entry]


Internal reports

  1. F. Besson, T. Jensen, D. Pichardie, and T. Turpin. Result certification for relational program analysis. Research Report 6333, Inria, September 2007. [WWW] [bibtex-entry]


  2. Frédéric Besson, Thomas Jensen, and Tiphaine Turpin. Computing stack maps with interfaces. Technical report 1879, Irisa, 2007. [WWW] [bibtex-entry]


  3. David Cachera, Thomas Jensen, and Pascal Sotin. Long-Run Cost Analysis by Approximation of Linear Operators over Dioids. Research Report 6338, INRIA, 10 2007. [WWW] [bibtex-entry]


  4. F. Besson, T. Jensen, and D. Pichardie. A PCC Architecture based on Certified Abstract Interpretation. Research Report RR-5751, INRIA, November 2005. Note: Also Publication Interne IRISA PI-1764. [PDF] [bibtex-entry]


  5. T. Jensen, D. Le Métayer, and T. Thorn. Verification of control flow based security policies. Technical report 1210, IRISA, 1998. [WWW] Keyword(s): security, verification, finite-state system, control flow, object orientation. [Abstract] [bibtex-entry]


Miscellaneous

  1. E. Denney, P. Fradet, C. Goire, T. Jensen, and D. Le Métayer. Procédé de vérification de transformateurs de codes pour un système embarqué, notamment sur une carte à puce, juillet 1999. Note: Brevet d'invention. [bibtex-entry]



BACK TO INDEX

This document was translated from BibTEX by bibtex2html