Thomas Jensen 

Campus de Beaulieu, 35042 Rennes, France
Tel: (+33 / 0) 2 99 84 74 78 
Fax: (+33 / 0) 2 99 84 71 71 

  • I'm head of the CELTIQUE research group, joint between INRIA, U. Rennes and ENS Cachan/Rennes.
  • I coordinate the ANR DeCert project on decision procedures and certification.
  • The Celtique team develops the Javalib and Sawja software tools, including parsers and static control flow analyzers for Java byte code.
  • Together with David Pichardie, I run the  Master's courses on semantics and static analysis and on software security at University of Rennes.


Directeur de recherche INRIA.

Cand. scient. in Computing and Mathematics, Univ. of Copenhagen,1990. PhD Imperial College, Univ. of London,1992. Habilitation à diriger des recherches, Univ. Rennes 1, 1999. In 1993 I joined the CNRS as Chargé de recherche at the Computing Laboratory at Ecole Polytechnique. From 1997, I have been affiliated with IRISA, Rennes where I became directeur de recherche CNRS in 2003 and was leader of the Lande research team 1999-2008. Since 2010 I am at INRIA where I am in charge of the newly created Celtique project on software certification through semantic analysis. 


Program analysis

Static program analysis aims at determining properties of the behaviour of a program without actually executing it. Static analysis is founded on the theory of abstract interpretation for proving the correctness of analyses with respect to the semantics of a programming language.
My work has among other things been concerned with
  • type-based static analysis
  • analyses for the particular language paradigms (in particular functional and object-oriented) 
  • control-flow analysis of programs, used e.g. in the activity on software security.
Recently, I have been investigating how static analysers can be designed using contructive logic in order to extract certified static analysers from their mechanically checked specifications.

Static analysis can be used to built a Proof-Carrying Code infrastructure where advanced static analysers can be used to construct program invariants that can be checked by simpler, and mechanically checked verifiers. Here is a paper describing such an architecture

Software security

The particular branch of information security called "language-based security"  is concerned with the study of programming language features for ensuring the security  of software. Programming languages such as Java offer a variety of language constructs for securing an application. Verifying that these constructs have been used properly to ensure a given security property is a challenge for program analysis,

I have been working of various versions of embbed Java, including Java Card and Java for mobile telephones. Here is an article (to appear in J. Computer Security) with a proposal for a more flexible access control mechanism for Java enabled moble telephones that is more amenable to static verification.

Java security can be further enhanced by extending the static byte code verification to other properties. At ByteCode 2009 I gave an invited talk   about how this can be made feasible using software certificates generated by static analysis. 



A full list of my publications as of  December 2012.