Computing stack maps with interfaces (2008)
Besson, Frédéric, Jensen, Thomas, Turpin, Tiphaine
Lightweight bytecode verification uses stack maps to annotate Java bytecode programs with type information in order to reduce the verification to type checking. This paper describes an improved...
Computing stack maps with interfaces (2008)
Besson, Frédéric, Jensen, Thomas, Turpin, Tiphaine
Lightweight bytecode verification uses stack maps to annotate Java bytecode programs with type information in order to reduce the verification to type checking. This paper describes an improved...
Semantic Foundations and Inference of Non-null Annotations (2008)
Hubert, Laurent, Jensen, Thomas, Pichardie, David
This paper proposes a semantics-based automatic null pointer analysis for inferring non-null annotations of fields in ob ject- oriented programs. The analysis is formulated for a minimalistic OO...
Semantic Foundations and Inference of Non-null Annotations (2008)
Hubert, Laurent, Jensen, Thomas, Pichardie, David
This paper proposes a semantics-based automatic null pointer analysis for inferring non-null annotations of fields in ob ject- oriented programs. The analysis is formulated for a minimalistic OO...
Computing stack maps with interfaces (2008)
Besson, Frédéric, Jensen, Thomas, Turpin, Tiphaine
Lightweigth byte code verification uses stack maps to annotate Java byte code programs with type information so that the byte code verifier (BCV) only has to check this typing, without having to do...
Computing stack maps with interfaces (2008)
Besson, Frédéric, Jensen, Thomas, Turpin, Tiphaine
Lightweigth byte code verification uses stack maps to annotate Java byte code programs with type information so that the byte code verifier (BCV) only has to check this typing, without having to do...
Circular reasoning rather than cyclic expression (2008)
Jensen, Lars, De Lichtenberg, Ulrik, Jensen, Thomas, Brunak, Søren, Bork, Peer
A response to Combined analysis reveals a core set of cycling genes by Y Lu, S Mahony, PV Benos, R Rosenfeld, I Simon, LL Breeden and Z Bar-Joseph. Genome Biol 2007, 8 :R146.
Rebranding in the service sector (2008)
JENSEN, THOMAS, OLSSON, FREDRIK, OSORIO, DANIEL
Thesis purpose: This thesis will through a case study of a recently rebranded bank âJyske Bankâ, seek to research deeper within the field of service sector rebranding. The internal...
Certifying a Tree Automata Completion Checker (2008)
Boyer, Benoît, Genet, Thomas, Jensen, Thomas
Tree automata completion is a technique for the verification of infinite state systems. It has already been used for the verification of cryptographic protocols and the prototyping of Java static...
Certifying a Tree Automata Completion Checker (2008)
Boyer, Benoît, Genet, Thomas, Jensen, Thomas
Tree automata completion is a technique for the verification of infinite state systems. It has already been used for the verification of cryptographic protocols and the prototyping of Java static...
Semantic foundations and inference of non-null annotations (2008)
Hubert, Laurent, Jensen, Thomas, Pichardie, David
This paper proposes a semantics-based automatic null pointer analysis for inferring non-null annotations of fields in object-oriented programs. The analysis is formulated for a minimalistic OO...
Semantic foundations and inference of non-null annotations (2008)
Hubert, Laurent, Jensen, Thomas, Pichardie, David
This paper proposes a semantics-based automatic null pointer analysis for inferring non-null annotations of fields in object-oriented programs. The analysis is formulated for a minimalistic OO...
Semantic foundations and inference of non-null annotations (2008)
Hubert, Laurent, Jensen, Thomas, Pichardie, David
This paper proposes a semantics-based automatic null pointer analysis for inferring non-null annotations of fields in object-oriented programs. The analysis is formulated for a minimalistic OO...
Semantic foundations and inference of non-null annotations (2008)
Hubert, Laurent, Jensen, Thomas, Pichardie, David
This paper proposes a semantics-based automatic null pointer analysis for inferring non-null annotations of fields in object-oriented programs. The analysis is formulated for a minimalistic OO...
Certifying a Tree Automata Completion Checker (2008)
Boyer, Benoît, Genet, Thomas, Jensen, Thomas
Tree automata completion is a technique for the verification of infinite state systems. It has already been used for the verification of cryptographic protocols and the prototyping of Java static...
Certifying a Tree Automata Completion Checker (2008)
Boyer, Benoît, Genet, Thomas, Jensen, Thomas
Tree automata completion is a technique for the verification of infinite state systems. It has already been used for the verification of cryptographic protocols and the prototyping of Java static...
Certifying a Tree Automata Completion Checker (2008)
Boyer, Benoît, Genet, Thomas, Jensen, Thomas
Tree automata completion is a technique for the verification of infinite state systems. It has already been used for the verification of cryptographic protocols and the prototyping of Java static...
Long-Run Cost Analysis byApproximation of Linear Operators over Dioids (2008)
Cachera, David, Jensen, Thomas, Jobin, Arnaud, Sotin, Pascal
We present a static analysis technique for modeling and approxi- mating the long-run resource usage of programs. The approach is based on a quantitative semantic framework where programs are...
Long-Run Cost Analysis byApproximation of Linear Operators over Dioids (2008)
Cachera, David, Jensen, Thomas, Jobin, Arnaud, Sotin, Pascal
We present a static analysis technique for modeling and approxi- mating the long-run resource usage of programs. The approach is based on a quantitative semantic framework where programs are...
Computing stack maps with interfaces (2007)
Besson, Frédéric, Jensen, Thomas, Turpin, Tiphaine
Lightweigth byte code verification uses stack maps to annotate Java byte code programs with type information so that the byte code verifier (BCV) only has to check this typing, without having to do...
Computing stack maps with interfaces (2007)
Besson, Frédéric, Jensen, Thomas, Turpin, Tiphaine
Lightweigth byte code verification uses stack maps to annotate Java byte code programs with type information so that the byte code verifier (BCV) only has to check this typing, without having to do...
Long-Run Cost Analysis byApproximation of Linear Operators over Dioids (2007)
Cachera, David, Jensen, Thomas, Sotin, Pascal
We present a static analysis technique for modeling and approxi- mating the long-run resource usage of programs. The approach is based on a quantitative semantic framework where programs are...
Long-Run Cost Analysis byApproximation of Linear Operators over Dioids (2007)
Cachera, David, Jensen, Thomas, Sotin, Pascal
We present a static analysis technique for modeling and approxi- mating the long-run resource usage of programs. The approach is based on a quantitative semantic framework where programs are...
Result certification for relational program analysis (2007)
Besson, Frédéric, Jensen, Thomas, Pichardie, David, Turpin, Tiphaine
We define a generic relational program analysis for an imperative, stack-oriented byte code language with procedures, arrays and global variables and instantiate it with an abstract domain of...
Result certification for relational program analysis (2007)
Besson, Frédéric, Jensen, Thomas, Pichardie, David, Turpin, Tiphaine
We define a generic relational program analysis for an imperative, stack-oriented byte code language with procedures, arrays and global variables and instantiate it with an abstract domain of...
Result certification for relational program analysis (2007)
Besson, Frédéric, Jensen, Thomas, Pichardie, David, Turpin, Tiphaine
We define a generic relational program analysis for an imperative, stack-oriented byte code language with procedures, arrays and global variables and instantiate it with an abstract domain of...
Result certification for relational program analysis (2007)
Besson, Frédéric, Jensen, Thomas, Pichardie, David, Turpin, Tiphaine
We define a generic relational program analysis for an imperative, stack-oriented byte code language with procedures, arrays and global variables and instantiate it with an abstract domain of...
Result certification for relational program analysis (2007)
Besson, Frédéric, Jensen, Thomas, Pichardie, David, Turpin, Tiphaine
We define a generic relational program analysis for an imperative, stack-oriented byte code language with procedures, arrays and global variables and instantiate it with an abstract domain of...
Result certification for relational program analysis (2007)
Besson, Frédéric, Jensen, Thomas, Pichardie, David, Turpin, Tiphaine
We define a generic relational program analysis for an imperative, stack-oriented byte code language with procedures, arrays and global variables and instantiate it with an abstract domain of...
Result certification for relational program analysis (2007)
Besson, Frédéric, Jensen, Thomas, Pichardie, David, Turpin, Tiphaine
We define a generic relational program analysis for an imperative, stack-oriented byte code language with procedures, arrays and global variables and instantiate it with an abstract domain of...
Result certification for relational program analysis (2007)
Besson, Frédéric, Jensen, Thomas, Pichardie, David, Turpin, Tiphaine
We define a generic relational program analysis for an imperative, stack-oriented byte code language with procedures, arrays and global variables and instantiate it with an abstract domain of...
Automata-based Confidentiality Monitoring (2007)
Le Guernic, Gurvan, Banerjee, Anindya, Jensen, Thomas, Schmidt, David
Non-interference is typically used as a baseline security policy to formalize confidentiality of secret information manipulated by a program. In contrast to static checking of non-interference, this...
Automata-based Confidentiality Monitoring (2007)
Le Guernic, Gurvan, Banerjee, Anindya, Jensen, Thomas, Schmidt, David
Non-interference is typically used as a baseline security policy to formalize confidentiality of secret information manipulated by a program. In contrast to static checking of non-interference, this...
Monitoring Information Flow (2007)
Le Guernic, Gurvan, Jensen, Thomas
We present an information flow monitoring mechanism for sequential programs. The monitor executes a program on standard data that are tagged with labels indicating their security level. We formalize...
Monitoring Information Flow (2007)
Le Guernic, Gurvan, Jensen, Thomas
We present an information flow monitoring mechanism for sequential programs. The monitor executes a program on standard data that are tagged with labels indicating their security level. We formalize...
A Formal Model of Access Control for Mobile Interactive Devices (2007)
Besson, Frédéric, Dufay, Guillaume, Jensen, Thomas
This paper presents an access control model for programming applications in which the access control to resources can employ user interaction to obtain the necessary permissions. This model is...
A Formal Model of Access Control for Mobile Interactive Devices (2007)
Besson, Frédéric, Dufay, Guillaume, Jensen, Thomas
This paper presents an access control model for programming applications in which the access control to resources can employ user interaction to obtain the necessary permissions. This model is...
Rewriting for Fast Prototyping of Static Analyzers (2007)
Boichut, Yohan, Genet, Thomas, Jensen, Thomas, Leroux, Luka
This paper defines a new framework for fast prototyping of static analyzers based on rewriting techniques. Starting from a term rewriting system representing the operational semantics of the target...
Rewriting for Fast Prototyping of Static Analyzers (2007)
Boichut, Yohan, Genet, Thomas, Jensen, Thomas, Leroux, Luka
This paper defines a new framework for fast prototyping of static analyzers based on rewriting techniques. Starting from a term rewriting system representing the operational semantics of the target...
A PCC Architecture based on Certified Abstract Interpretation (2007)
Besson, Frédéric, Jensen, Thomas, Pichardie, David
Proof Carrying Code (PCC) is a technique for downloading mobile code on a host machine while ensuring that the code adheres to the host's security policy. We show how certified abstract...
A PCC Architecture based on Certified Abstract Interpretation (2007)
Besson, Frédéric, Jensen, Thomas, Pichardie, David
Proof Carrying Code (PCC) is a technique for downloading mobile code on a host machine while ensuring that the code adheres to the host's security policy. We show how certified abstract...
A PCC Architecture based on Certified Abstract Interpretation (2007)
Besson, Frédéric, Jensen, Thomas, Pichardie, David
Proof Carrying Code (PCC) is a technique for downloading mobile code on a host machine while ensuring that the code adheres to the host's security policy. We show how certified abstract...
A PCC Architecture based on Certified Abstract Interpretation (2007)
Besson, Frédéric, Jensen, Thomas, Pichardie, David
Proof Carrying Code (PCC) is a technique for downloading mobile code on a host machine while ensuring that the code adheres to the host's security policy. We show how certified abstract...
A Formal Model of Access Control for Mobile Interactive Devices (2006)
Besson, Frédéric, Dufay, Guillaume, Jensen, Thomas
Abstract. This paper presents an access control model for programming applications in which the access control to resources can employ user interaction to obtain the necessary permissions. This model...
Rewriting for Fast Prototyping of Static Analyzers (2006)
Boichut, Yohan, Genet, Thomas, Jensen, Thomas, Le Roux, Luka
This paper defines a new framework for fast prototyping of static analyzers based on rewriting techniques. Starting from a term rewriting system representing the operational semantics of the target...
Rewriting for Fast Prototyping of Static Analyzers (2006)
Boichut, Yohan, Genet, Thomas, Jensen, Thomas, Le Roux, Luka
This paper defines a new framework for fast prototyping of static analyzers based on rewriting techniques. Starting from a term rewriting system representing the operational semantics of the target...
Rewriting for Fast Prototyping of Static Analyzers (2006)
Boichut, Yohan, Genet, Thomas, Jensen, Thomas, Le Roux, Luka
This paper defines a new framework for fast prototyping of static analyzers based on rewriting techniques. Starting from a term rewriting system representing the operational semantics of the target...
A PCC Architecture based on Certified Abstract Interpretation (2005)
Besson, Frédéric, Jensen, Thomas, Pichardie, David
Proof Carrying Code (PCC) is a technique for downloading mobile code on a host machine while ensuring that the code adheres to the host's security policy. We show how certified abstract...
Monitoring Information Flow (2005)
Le Guernic, Gurvan, Jensen, Thomas
We present an information flow monitoring mechanism for sequential programs. The monitor executes a program on standard data that are tagged with labels indicating their security level. We formalize...
ATOMIC CASCADE IN KAONIC HYDROGEN AND DEUTERIUM (2005)
The atomic cascade in kaonic hydrogen and deuterium has been studied in the extended standard cascade model. We discuss predictions of $K$ x--ray yields in relation to experimental data and the...
ATOMIC CASCADE IN KAONIC HYDROGEN AND DEUTERIUM (2005)
The atomic cascade in kaonic hydrogen and deuterium has been studied in the extended standard cascade model. We discuss predictions of $K$ x--ray yields in relation to experimental data and the...
A PCC Architecture based on Certified Abstract Interpretation (2005)
Besson, Frédéric, Jensen, Thomas, Pichardie, David
Proof Carrying Code (PCC) is a technique for downloading mobile code on a host machine while ensuring that the code adheres to the host's security policy. We show how certified abstract...
Extracting a Data Flow Analyser in (2004)
David Cachera, Thomas Jensen, David Pichardie, Vlad Rusu
We show how to formalise a constraint-based data flow analysis in the specification language of the Coq proof assistant. This involves defining a dependent type of lattices together with a library of...
Kinetic energy distributions in pionic hydrogen (2004)
A framework for analyzing the Doppler broadening of the x--ray lines in pionic hydrogen is proposed. It is shown that the kinetic energy distributions at the instant of the $np\to1s$ ($n=2-4$)...
ATOMIC CASCADE IN KAONIC HYDROGEN AND DEUTERIUM (2004)
The atomic cascade in kaonic hydrogen and deuterium has been studied in the extended standard cascade model. We discuss predictions of $K$ x--ray yields in relation to experimental data and the...
ATOMIC CASCADE IN KAONIC HYDROGEN AND DEUTERIUM (2004)
The atomic cascade in kaonic hydrogen and deuterium has been studied in the extended standard cascade model. We discuss predictions of $K$ x--ray yields in relation to experimental data and the...
Electronic Notes in Theoretical Computer Science 82 No. 2 (2003) (2003)
Thomas Genet, Thomas Jensen, Vikash Kodati, David Pichardie
The Java Card language is a trimmed down dialect of Java aimed at programming smart cards. Java Card speci es its own class le format (the Java Card Converted APplet (CAP) format) that is optimised...
Construction Correcte de Logiciels pour Carte a Puce (2002)
Ludovic Casset, De La Mediterranee, Jonathan Bowen Professeur, Didier Bert, Thomas Jensen, ...
Nous proposons dans cette thèse de développer une méthodologie quant à lutilisation industrielle de la méthode B dans le domaine des cartes à puce. Pour cela, ce document se décompose en six...
Constraint-based security analysis for the Java Card firewall (2002)
This paper presents a constraint-based static analysis to prove security (confidentiality) properties of Java Card programs. We define a subset of the Java Card bytecode focussing on aspects of the...
A Formal Specification of the Java Card Firewall (2002)
this paper is to provide a formal speci cation of the Java Card rewall, a mechanism designed to protect the security and integrity of the Java Card Runtime Environment (JCRE) and of each applet. In...
Analyse Statique De Programmes : Fondements Et Applications (2000)
Thomas Jensen, M. Jean-pierre, Bantre Prsident, Mm Nicolas, Neil Jones, Giorgio Levi, ...
domains . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.2.2 Lattices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 1.2.3 Specification of analyses . . . . . . . . . . ....
Correctness of Java Card Method Lookup via Logical Relations (2000)
This article presents a formalisation of the bytecode optimisation of Sun's Java Card language from the class file to CAP file format as a set of constraints between the two formats, and defines and...
An Overview of Class Analyses of Object-oriented Languages (2000)
The nice features of object-oriented programming often lead to runtime inefficiency. In particular, late binding does not allow to bind statically a method invocation with its code. Information about...
Correctness of Java Card Method Lookup via Logical Relations (2000)
. We formalise the Java Card bytecode optimisation from class file to CAP file format as a set of constraints between the two formats, and define and prove its correctness. Java Card bytecode is...
Correctness of Java Card Method Lookup via Logical Relations (Extended Abstract) (2000)
We present a formalisation of the bytecode optimisation of Sun's Java Card language from the class file to CAP file format as a set of constraints between the two formats, and define and prove its...
Polyhedral Analysis for Synchronous Languages (1999)
Thomas Jensen, Jean-pierre Talpin
. We define an operational semantics for the Signal language and design an analysis which allows to verify properties pertaining to the relation between values of the numeric and boolean variables of...
Polyhedral Analysis for Synchronous Languages (1999)
Thomas Jensen, Jean-pierre Talpin
. We define an operational semantics for the Signal language and design an analysis which allows to verify properties pertaining to the relation between values of the numeric and boolean variables of...
Thesis directed by Alan L. Johnson for the Department of Biological Sciences.
Thesis (Ph. D.)--University of Notre Dame; July, 1999.
Thesis (doctoral)--Universität Hamburg, 1997.
Mikrofiche-Ausg.: 1 Mikrofiche : 24x.
Projection Effects and Strategic Ambiguity in Electoral Competition
Theories from psychology suggest that voters' perceptions of political positions depend on their non-policy related attitudes towards the candidates. A voter who likes (dislikes) a candidate will...
Elections, Private Information, and State-Dependent Candidate Quality
In this paper we contribute to the study of how democracy works when politicians are better informed than the electorate about conditions relevant for policy choice. We do so by setting up and...
Terrorism, Anti-Terrorism, and the Copycat Effect
In this paper we contribute to the study of how democracy works when politicians are better informed than the electorate about conditions relevant for policy choice. We do so by setting up and...
Can Ambiguity in Electoral Competition be Explained by Projection Effects in Voters' Perceptions?
Studies in political science and psychology suggest that voters' perceptions of political positions depend on their personal views of the candidates. A voter who likes/dislikes a candidate will...
Skov, Vibe, Glintborg, Dorte, Knudsen, Steen, Tan, Qihua, Jensen, Thomas, Kruse, Torben A., ...
Insulin resistance is a common metabolic abnormality in women with PCOS and leads to an elevated risk of type 2 diabetes. Studies have shown that thiazolidinediones (TZDs) improve metabolic...