default search action
Thomas P. Jensen
Person information
- affiliation: Inria, Rennes, France
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
- [j22]Andrzej Filinski
, Ken Friis Larsen
Axiomatising an information flow logic based on partial equivalence relations. Int. J. Softw. Tools Technol. Transf. 26(4): 445-461 (2024) - 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
MichelsonLiSA: A Static Analyzer for Tezos. PerCom Workshops 2023: 80-85 - [c72]Gautier Raimondi
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
Lifting Numeric Relational Domains to Algebraic Data Types. SAS 2022: 104-134 - 2021
- [j21]Ahmad Salim Al-Sibahi
Verification of Program Transformations with Inductive Refinement Types. ACM Trans. Softw. Eng. Methodol. 30(1): 5:1-5:33 (2021) - [c69]Benoît Montagu
Trace-based control-flow analysis. PLDI 2021: 482-496 - 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
Stable relations and abstract interpretation of higher-order programs. Proc. ACM Program. Lang. 4(ICFP): 119:1-119:30 (2020) - [c68]Ahmad Salim Al-Sibahi
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
2010 – 2019
- 2019
- [j18]Martin Bodin
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) - [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
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
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 - [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
- [c60]Frédéric Besson, Nataliia Bielova
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 - [i3]Nataliia Bielova, Frédéric Besson, Thomas P. Jensen:
Using JavaScript Monitoring to Prevent Device Fingerprinting. ERCIM News 2016(106) (2016) - 2015
- [c58]Martin Bodin
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
Hybrid Typing of Secure Information Flow in a JavaScript-Like Language. TGC 2015: 63-78 - [e4]Sandrine Blazy
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] - 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) - [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
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
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
Pretty-big-step-semantics-based Certified Abstract Interpretation (Preliminary version). Festschrift for Dave Schmidt 2013: 360-383 - 2012
- [j15]Thomas P. Jensen, Florent Kirchner, David Pichardie:
Secure the Clones. Log. Methods Comput. Sci. 8(2) (2012) - [j14]Jan Midtgaard
Control-flow analysis of function calls and returns by abstract interpretation. Inf. Comput. 211: 49-76 (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
- [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) - [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 - [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)
2000 – 2009
- 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
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
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
- [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) - [c33]Gurvan Le Guernic
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
- [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) - [c29]David Cachera, Thomas P. Jensen, David Pichardie, Gerardo Schneider:
Certified Memory Usage Analysis. FM 2005: 91-106 - [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] - 2004
- [j8]Marieke Huisman
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) - [c28]David Cachera, Thomas P. Jensen, David Pichardie, Vlad Rusu:
Extracting a Data Flow Analyser in Constructive Logic. ESOP 2004: 385-400 - 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
Class analyses as abstract interpretations of trace semantics. ACM Trans. Program. Lang. Syst. 25(5): 578-630 (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
- [j4]Ewen Denney, Thomas P. Jensen:
Correctness of Java card method lookup via logical relations. Theor. Comput. Sci. 283(2): 305-331 (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
- [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) - [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 - [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] - 2000
- [c19]Ewen Denney, Thomas P. Jensen:
Correctness of Java Card Method Lookup via Logical Relations. ESOP 2000: 104-118
1990 – 1999
- 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 - 1997
- [j2]Thomas P. Jensen:
Disjunctive Program Analysis for Algebraic Data Types. ACM Trans. Program. Lang. Syst. 19(5): 751-803 (1997) - 1996
- [c13]Thomas P. Jensen, Ian Mackie:
Flow Analysis in the Geometry of Interaction. ESOP 1996: 188-203 - 1995
- [j1]Thomas P. Jensen:
Conjunctive Type Systems and Abstract Interpretation of Higher-Order Functional Programs. J. Log. Comput. 5(4): 397-421 (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
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
Coauthor Index
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-10-07 21:23 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: