Thomas Jensen 

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

  • Head of the CELTIQUE research group, joint between INRIA, U. Rennes and ENS Rennes.
  • I coordinate the Security track of Labex Comin Labs, and participate in the ANR projects Ajacs and ANASTASEC.
  • I was chairman of the 22nd International
    Static Analysis Symposium, held in Saint-Malo in September 2015.
  • Together with Delphine Demange, I teach the  Master's courses on semantics and static analysis and on software security at University of Rennes.
  • The Celtique team develops the Javalib and Sawja software tools, including parsers and static control flow analyzers for Java byte code.


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  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
  • certification of static analysis

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 embedded Java, including Java Card and Java for mobile telephones. Java security can be further enhanced by extending the static byte code verification to other properties. The  SAWJACard project developed a tool for certifying Java Card applications according to NFC industry norms.

In another strand of work, I am interested in mixing static and dynamic program analysis for precise information flow control. Such hybrid analysis aims at computing a precise estimation of attacker knowledge, with application eg. to identification of web tracking scripts.