![](https://dblp.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
default search action
Thomas P. Jensen
Person information
- affiliation: Inria, Rennes, France
Refine list
![note](https://dblp.uni-trier.de/img/note-mark.dark.12x12.png)
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
Journal Articles
- 2021
- [j21]Ahmad Salim Al-Sibahi
, Thomas P. Jensen
, Aleksandar S. Dimovski
, Andrzej Wasowski
:
Verification of Program Transformations with Inductive Refinement Types. ACM Trans. Softw. Eng. Methodol. 30(1): 5:1-5:33 (2021) - 2020
- [j20]Timothée Haudebourg, Thomas Genet, Thomas P. Jensen:
Regular language type inference with term rewriting. Proc. ACM Program. Lang. 4(ICFP): 112:1-112:29 (2020) - [j19]Benoît Montagu
, Thomas P. Jensen:
Stable relations and abstract interpretation of higher-order programs. Proc. ACM Program. Lang. 4(ICFP): 119:1-119:30 (2020) - 2019
- [j18]Martin Bodin
, Philippa Gardner, Thomas P. Jensen, Alan Schmitt:
Skeletal semantics and their interpretations. Proc. ACM Program. Lang. 3(POPL): 44:1-44:31 (2019) - [j17]Oana Fabiana Andreescu, Thomas P. Jensen, Stéphane Lescuyer, Benoît Montagu
:
Inferring frame conditions with static correlation analysis. Proc. ACM Program. Lang. 3(POPL): 47:1-47:29 (2019) - 2014
- [j16]David Cachera, Thomas P. Jensen, Arnaud Jobin, Florent Kirchner:
Inference of polynomial invariants for imperative programs: A farewell to Gröbner bases. Sci. Comput. Program. 93: 89-109 (2014) - 2012
- [j15]Thomas P. Jensen, Florent Kirchner, David Pichardie:
Secure the Clones. Log. Methods Comput. Sci. 8(2) (2012) - [j14]Jan Midtgaard
, Thomas P. Jensen:
Control-flow analysis of function calls and returns by abstract interpretation. Inf. Comput. 211: 49-76 (2012) - 2010
- [j13]Frédéric Besson, Guillaume Dufay, Thomas P. Jensen, David Pichardie:
Verifying resource access control on mobile interactive devices. J. Comput. Secur. 18(6): 971-998 (2010) - [j12]David Cachera, Thomas P. Jensen, Arnaud Jobin, Pascal Sotin:
Long-run cost analysis by approximation of linear operators over dioids. Math. Struct. Comput. Sci. 20(4): 589-624 (2010) - 2006
- [j11]Frédéric Besson, Thomas P. Jensen, David Pichardie:
Proof-carrying code from certified abstract interpretation and fixpoint compression. Theor. Comput. Sci. 364(3): 273-291 (2006) - 2005
- [j10]Frédéric Besson, Thomas de Grenier de Latour, Thomas P. Jensen:
Interfaces for stack inspection. J. Funct. Program. 15(2): 179-217 (2005) - [j9]David Cachera, Thomas P. Jensen, David Pichardie, Vlad Rusu:
Extracting a data flow analyser in constructive logic. Theor. Comput. Sci. 342(1): 56-78 (2005) - 2004
- [j8]Marieke Huisman
, Thomas P. Jensen:
Guest editors' introduction: Special issue on Formal Methods for Smart Cards. J. Log. Algebraic Methods Program. 58(1-2): 1-2 (2004) - [j7]Marc Éluard, Thomas P. Jensen:
Validation du contrôle d'accès dans des cartes à puce multiapplications. Tech. Sci. Informatiques 23(3): 323-357 (2004) - 2003
- [j6]Anindya Banerjee, Thomas P. Jensen:
Modular Control-Flow Analysis with Rank 2 Intersection Types. Math. Struct. Comput. Sci. 13(1): 87-124 (2003) - [j5]Fausto Spoto
, Thomas P. Jensen:
Class analyses as abstract interpretations of trace semantics. ACM Trans. Program. Lang. Syst. 25(5): 578-630 (2003) - 2002
- [j4]Ewen Denney, Thomas P. Jensen:
Correctness of Java card method lookup via logical relations. Theor. Comput. Sci. 283(2): 305-331 (2002) - 2001
- [j3]Frédéric Besson, Thomas P. Jensen, Daniel Le Métayer:
Model Checking Security Properties of Control Flow Graphs. J. Comput. Secur. 9(3): 217-250 (2001) - 1997
- [j2]Thomas P. Jensen:
Disjunctive Program Analysis for Algebraic Data Types. ACM Trans. Program. Lang. Syst. 19(5): 751-803 (1997) - 1995
- [j1]Thomas P. Jensen:
Conjunctive Type Systems and Abstract Interpretation of Higher-Order Functional Programs. J. Log. Comput. 5(4): 397-421 (1995)
Conference and Workshop Papers
- 2023
- [c74]Théo Losekoot, Thomas Genet, Thomas P. Jensen:
Automata-Based Verification of Relational Properties of Functions over Algebraic Data Structures. FSCD 2023: 7:1-7:22 - [c73]Luca Olivieri
, Thomas P. Jensen, Luca Negrini
, Fausto Spoto:
MichelsonLiSA: A Static Analyzer for Tezos. PerCom Workshops 2023: 80-85 - [c72]Gautier Raimondi
, Frédéric Besson
, Thomas P. Jensen
:
Type-directed Program Transformation for Constant-Time Enforcement. PPDP 2023: 6:1-6:13 - [c71]Thomas P. Jensen, Vincent Rebiscoul, Alan Schmitt:
Deriving Abstract Interpreters from Skeletal Semantics. EXPRESS/SOS 2023: 97-113 - 2022
- [c70]Santiago Bautista
, Thomas P. Jensen
, Benoît Montagu
:
Lifting Numeric Relational Domains to Algebraic Data Types. SAS 2022: 104-134 - 2021
- [c69]Benoît Montagu
, Thomas P. Jensen:
Trace-based control-flow analysis. PLDI 2021: 482-496 - 2020
- [c68]Ahmad Salim Al-Sibahi
, Thomas P. Jensen
, Rasmus Ejlers Møgelberg, Andrzej Wasowski
:
Galois Connections for Recursive Types. From Lambda Calculus to Cybersecurity Through Program Analysis 2020: 105-131 - [c67]Thomas Genet, Thomas P. Jensen, Justine Sauvage:
Termination of Ethereum's Smart Contracts. ICETE (2) 2020: 39-51 - 2019
- [c66]Frédéric Besson, Alexandre Dang, Thomas P. Jensen:
Information-Flow Preservation in Compiler Optimisations. CSF 2019: 230-242 - [c65]Frédéric Besson
, Sandrine Blazy
, Alexandre Dang, Thomas P. Jensen, Pierre Wilke
:
Compiling Sandboxes: Formally Verified Software Fault Isolation. ESOP 2019: 499-524 - 2018
- [c64]Frédéric Besson, Alexandre Dang, Thomas P. Jensen:
Securing Compilation Against Memory Probing. PLAS@CCS 2018: 29-40 - [c63]Thomas Genet, Timothée Haudebourg, Thomas P. Jensen:
Verifying Higher-Order Functions with Tree Automata. FoSSaCS 2018: 565-582 - [c62]Ahmad Salim Al-Sibahi
, Thomas P. Jensen, Aleksandar S. Dimovski
, Andrzej Wasowski
:
Verification of high-level transformations with inductive refinement types. GPCE 2018: 147-160 - [c61]Frédéric Besson, Thomas P. Jensen, Julien Lepiller
:
Modular Software Fault Isolation as Abstract Interpretation. SAS 2018: 166-186 - 2016
- [c60]Frédéric Besson, Nataliia Bielova
, Thomas P. Jensen:
Hybrid Monitoring of Attacker Knowledge. CSF 2016: 225-238 - [c59]Oana Fabiana Andreescu, Thomas P. Jensen, Stéphane Lescuyer:
Correlating Structured Inputs and Outputs in Functional Specifications. SEFM 2016: 85-103 - 2015
- [c58]Martin Bodin
, Thomas P. Jensen, Alan Schmitt:
Certified Abstract Interpretation with Pretty-Big-Step Semantics. CPP 2015: 29-40 - [c57]Oana Fabiana Andreescu, Thomas P. Jensen, Stéphane Lescuyer:
Dependency Analysis of Functional Specifications with Algebraic Data Structures. ICFEM 2015: 116-133 - [c56]José Fragoso Santos
, Thomas P. Jensen, Tamara Rezk, Alan Schmitt:
Hybrid Typing of Secure Information Flow in a JavaScript-Like Language. TGC 2015: 63-78 - 2014
- [c55]Martin Bodin, Thomas P. Jensen, Alan Schmitt:
Pretty-big-step-semantics-based Certified Abstract Interpretation. JFLA 2014: 109-130 - [c54]Frédéric Besson, Nataliia Bielova
, Thomas P. Jensen:
Browser Randomisation against Fingerprinting: A Quantitative Information Flow Approach. NordSec 2014: 181-196 - [c53]Frédéric Besson, Thomas P. Jensen, Pierre Vittet:
SawjaCard: A Static Analysis Tool for Certifying Java Card Applications. SAS 2014: 51-67 - 2013
- [c52]Frédéric Besson, Nataliia Bielova
, Thomas P. Jensen:
Hybrid Information Flow Monitoring against Web Tracking. CSF 2013: 240-254 - [c51]Frédéric Besson, Pierre-Emmanuel Cornilleau, Thomas P. Jensen:
Result Certification of Static Program Analysers with Automated Theorem Provers. VSTTE 2013: 304-325 - [c50]Martin Bodin
, Thomas P. Jensen, Alan Schmitt:
Pretty-big-step-semantics-based Certified Abstract Interpretation (Preliminary version). Festschrift for Dave Schmidt 2013: 360-383 - 2012
- [c49]David Cachera, Thomas P. Jensen, Arnaud Jobin, Florent Kirchner:
Inference of Polynomial Invariants for Imperative Programs: A Farewell to Gröbner Bases. SAS 2012: 58-74 - 2011
- [c48]Thomas P. Jensen, Florent Kirchner, David Pichardie:
Secure the Clones - Static Enforcement of Policies for Secure Object Copying. ESOP 2011: 317-337 - 2010
- [c47]Delphine Demange, Thomas P. Jensen, David Pichardie:
A Provably Correct Stackless Intermediate Representation for Java Bytecode. APLAS 2010: 97-113 - [c46]Laurent Hubert, Thomas P. Jensen, Vincent Monfort, David Pichardie:
Enforcing Secure Object Initialization in Java. ESORICS 2010: 101-115 - [c45]Laurent Hubert, Nicolas Barré, Frédéric Besson, Delphine Demange, Thomas P. Jensen, Vincent Monfort, David Pichardie, Tiphaine Turpin:
Sawja: Static Analysis Workshop for Java. FoVeOOS 2010: 92-106 - [c44]Frédéric Besson, Thomas P. Jensen, David Pichardie, Tiphaine Turpin:
Certified Result Checking for Polyhedral Analysis of Bytecode Programs. TGC 2010: 253-267 - 2009
- [c43]Frédéric Besson, David Cachera, Thomas P. Jensen, David Pichardie:
Certified Static Analysis by Abstract Interpretation. FOSAD 2009: 223-257 - [c42]Jan Midtgaard
, Thomas P. Jensen:
Control-flow analysis of function calls and returns by abstract interpretation. ICFP 2009: 287-298 - 2008
- [c41]David Cachera, Thomas P. Jensen, Arnaud Jobin, Pascal Sotin:
Long-Run Cost Analysis by Approximation of Linear Operators over Dioids. AMAST 2008: 122-138 - [c40]Benoît Boyer, Thomas Genet, Thomas P. Jensen:
Certifying a Tree Automata Completion Checker. IJCAR 2008: 523-538 - [c39]Frédéric Besson, Thomas P. Jensen, Tiphaine Turpin:
Computing Stack Maps with Interfaces. ECOOP 2008: 642-666 - [c38]Laurent Hubert, Thomas P. Jensen, David Pichardie:
Semantic Foundations and Inference of Non-null Annotations. FMOODS 2008: 132-149 - [c37]Jan Midtgaard
, Thomas P. Jensen:
A Calculational Approach to Control-Flow Analysis by Abstract Interpretation. SAS 2008: 347-362 - 2007
- [c36]Frédéric Besson, Thomas P. Jensen, Tiphaine Turpin:
Small Witnesses for Abstract Interpretation-Based Proofs. ESOP 2007: 268-283 - [c35]Gilles Barthe, Pierre Crégut, Benjamin Grégoire, Thomas P. Jensen, David Pichardie:
The MOBIUS Proof Carrying Code Infrastructure. FMCO 2007: 1-24 - [c34]Yohan Boichut, Thomas Genet, Thomas P. Jensen, Luka Le Roux:
Rewriting Approximations for Fast Prototyping of Static Analyzers. RTA 2007: 48-62 - 2006
- [c33]Gurvan Le Guernic
, Anindya Banerjee, Thomas P. Jensen, David A. Schmidt:
Automata-Based Confidentiality Monitoring. ASIAN 2006: 75-89 - [c32]Frédéric Besson, Guillaume Dufay, Thomas P. Jensen:
A Formal Model of Access Control for Mobile Interactive Devices. ESORICS 2006: 110-126 - [c31]Thomas P. Jensen:
Certificates of Resource Usage on Mobile Telephones. ISoLA 2006: 6-7 - [c30]Pascal Sotin, David Cachera, Thomas P. Jensen:
Quantitative Static Analysis Over Semirings: Analysing Cache Behaviour for Java Card. QAPL 2006: 153-167 - 2005
- [c29]David Cachera, Thomas P. Jensen, David Pichardie, Gerardo Schneider:
Certified Memory Usage Analysis. FM 2005: 91-106 - 2004
- [c28]David Cachera, Thomas P. Jensen, David Pichardie, Vlad Rusu:
Extracting a Data Flow Analyser in Constructive Logic. ESOP 2004: 385-400 - 2003
- [c27]Frédéric Besson, Thomas P. Jensen:
Modular Class Analysis with DATALOG. SAS 2003: 19-36 - [c26]Thomas Genet, Thomas P. Jensen, Vikash Kodati, David Pichardie:
A Java Card CAP converter in PVS. COCV@ETAPS 2003: 426-442 - 2002
- [c25]Thomas P. Jensen:
Types in Program Analysis. The Essence of Computation 2002: 204-222 - [c24]Marc Éluard, Thomas P. Jensen:
Secure Object Flow Analysis for Java Card. CARDIS 2002: 97-110 - [c23]Thomas P. Jensen, Florimond Ployette, Olivier Ridoux:
Iteration schemes for fixed point calculation. FICS 2002: 69-76 - [c22]Frédéric Besson, Thomas de Grenier de Latour, Thomas P. Jensen:
Secure calling contexts for stack inspection. PPDP 2002: 76-87 - 2001
- [c21]Marc Éluard, Thomas P. Jensen, Ewen Denney:
An Operational Semantics of the Java Card Firewall. E-smart 2001: 95-110 - [c20]Thomas P. Jensen, Fausto Spoto
:
Class Analysis of Object-Oriented Programs through Abstract Interpretation. FoSSaCS 2001: 261-275 - 2000
- [c19]Ewen Denney, Thomas P. Jensen:
Correctness of Java Card Method Lookup via Logical Relations. ESOP 2000: 104-118 - 1999
- [c18]Frédéric Besson, Thomas P. Jensen, Jean-Pierre Talpin:
Polyhedral Analysis for Synchronous Languages. SAS 1999: 51-68 - [c17]Thomas P. Jensen, Daniel Le Métayer, Tommy Thorn:
Verification of Control Flow based Security Properties. S&P 1999: 89-103 - 1998
- [c16]Thomas P. Jensen, Daniel Le Métayer, Tommy Thorn:
Coarse Grained Java Security Policies. ECOOP Workshops 1998: 296 - [c15]Thomas P. Jensen, Daniel Le Métayer, Tommy Thorn:
Security and Dynamic Class Loading in Java: A Formalization. ICCL 1998: 4-15 - [c14]Thomas P. Jensen:
Inference of Polymorphic and Conditional Strictness Properties. POPL 1998: 209-221 - 1996
- [c13]Thomas P. Jensen, Ian Mackie:
Flow Analysis in the Geometry of Interaction. ESOP 1996: 188-203 - 1995
- [c12]Thomas P. Jensen:
Clock Analysis of Synchronous Dataflow Programs. PEPM 1995: 156-167 - 1994
- [c11]Thomas P. Jensen:
Abstract Interpretation over Algebraic Data Types. ICCL 1994 - [c10]Thomas P. Jensen:
Denotational Semantics of Timed Dataflow Programs. Theory and Formal Methods 1994: 381-396 - 1993
- [c9]Lindsay Errington, Chris Hankin, Thomas P. Jensen:
Reasoning About Gamma Programs. Theory and Formal Methods 1993: 115-125 - [c8]Lindsay Errington, Chris Hankin, Thomas P. Jensen:
A Congruence for Gamma Programs. WSA 1993: 242-253 - 1992
- [c7]Eric Goubault, Thomas P. Jensen:
Homology of Higher Dimensional Automata. CONCUR 1992: 254-268 - [c6]Thomas P. Jensen:
Disjunctive Strictness Analysis. LICS 1992: 174-185 - [c5]Thomas P. Jensen:
Axiomatising Uniform Properties of Recursive Data Structures. WSA 1992: 144-151 - 1991
- [c4]Thomas P. Jensen:
Strictness Analysis in Logical Form. FPCA 1991: 352-366 - [c3]Samson Abramsky
, Thomas P. Jensen:
A Relational Approach to Strictness Analysis for Higher-Order Polymorphic Functions. POPL 1991: 49-54 - 1990
- [c2]Thomas P. Jensen, Torben Æ. Mogensen:
A Backwards Analysis for Compile-time Garbage Collection. ESOP 1990: 227-239 - [c1]Thomas P. Jensen:
Abstract Interpretation vs. Type Inference A Topological Perspective. Functional Programming 1990: 141-145
Editorship
- 2015
- [e4]Sandrine Blazy
, Thomas P. Jensen:
Static Analysis - 22nd International Symposium, SAS 2015, Saint-Malo, France, September 9-11, 2015, Proceedings. Lecture Notes in Computer Science 9291, Springer 2015, ISBN 978-3-662-48287-2 [contents] - 2005
- [e3]Michael D. Ernst, Thomas P. Jensen:
Proceedings of the 2005 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis For Software Tools and Engineering, PASTE'05, Lisbon, Portugal, September 5-6, 2005. ACM 2005, ISBN 1-59593-239-9 [contents] - 2001
- [e2]Isabelle Attali, Thomas P. Jensen:
Smart Card Programming and Security, International Conference on Research in Smart Cards, E-smart 2001, Cannes, France, September 19-21, 2001, Proceedings. Lecture Notes in Computer Science 2140, Springer 2001, ISBN 3-540-42610-8 [contents] - [e1]Isabelle Attali, Thomas P. Jensen:
Java on Smart Cards: Programming and Security, First International Workshop, JavaCard 2000, Cannes, France, September 14, 2000, Revised Papers. Lecture Notes in Computer Science 2041, Springer 2001, ISBN 3-540-42167-X [contents]
Informal and Other Publications
- 2018
- [i5]Ahmad Salim Al-Sibahi, Thomas P. Jensen, Aleksandar S. Dimovski, Andrzej Wasowski:
Verification of High-Level Transformations with Inductive Refinement Types. CoRR abs/1809.06336 (2018) - [i4]Martin Bodin, Philippa Gardner, Thomas P. Jensen, Alan Schmitt:
Skeletal Semantics and their Interpretations. CoRR abs/1809.09749 (2018) - 2016
- [i3]Nataliia Bielova, Frédéric Besson, Thomas P. Jensen:
Using JavaScript Monitoring to Prevent Device Fingerprinting. ERCIM News 2016(106) (2016) - 2010
- [i2]Laurent Hubert, Thomas P. Jensen, Vincent Monfort, David Pichardie:
Enforcing Secure Object Initialization in Java. CoRR abs/1007.3133 (2010) - [i1]Laurent Hubert, Nicolas Barré, Frédéric Besson, Delphine Demange, Thomas P. Jensen, Vincent Monfort, David Pichardie, Tiphaine Turpin:
Sawja: Static Analysis Workshop for Java. CoRR abs/1007.3353 (2010)
Coauthor Index
![](https://dblp.uni-trier.de/img/cog.dark.24x24.png)
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-05-08 21:49 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint