A Backwards Analysis for Compile-time Garbage Collection. - Thomas P. Jensen; Torben Æ. Mogensen (ESOP, 1990)

Abstract Interpretation vs. Type Inference A Topological Perspective. - Thomas P. Jensen (Functional Programming, 1990)

Strictness Analysis in Logical Form. - Thomas P. Jensen (FPCA, 1991)

A Relational Approach to Strictness Analysis for Higher-Order Polymorphic Functions. - Samson Abramsky; Thomas P. Jensen (POPL, 1991)

Homology of Higher Dimensional Automata. - Eric Goubault; Thomas P. Jensen (CONCUR, 1992)

Disjunctive Strictness Analysis - Thomas P. Jensen (LICS, 1992)

Axiomatising Uniform Properties of Recursive Data Structures. - Thomas P. Jensen (WSA, 1992)

Reasoning About Gamma Programs. - Lindsay Errington; Chris Hankin; Thomas P. Jensen (Theory and Formal Methods, 1993)

A Congruence for Gamma Programs. - Lindsay Errington; Chris Hankin; Thomas P. Jensen (WSA, 1993)

Abstract Interpretation over Algebraic Data Types. - Thomas P. Jensen (ICCL, 1994)

Denotational Semantics of Timed Dataflow Programs. - Thomas P. Jensen (Theory and Formal Methods, 1994)

Clock Analysis of Synchronous Dataflow Programs. - Thomas P. Jensen (PEPM, 1995)

Conjunctive Type Systems and Abstract Interpretation of Higher-Order Functional Programs. - Thomas P. Jensen (J. Log. Comput., 1995)

Flow Analysis in the Geometry of Interaction. - Thomas P. Jensen; Ian Mackie (ESOP, 1996)

Disjunctive Program Analysis for Algebraic Data Types. - Thomas P. Jensen (ACM Trans. Program. Lang. Syst., 1997)

Coarse Grained Java Security Policies. - Thomas P. Jensen; Daniel Le Métayer; Tommy Thorn (ECOOP Workshops, 1998)

Security and Dynamic Class Loading in Java: A Formalization. - Thomas P. Jensen; Daniel Le Métayer; Tommy Thorn (ICCL, 1998)

Inference of Polymorphic and Conditional Strictness Properties. - Thomas P. Jensen (POPL, 1998)

Polyhedral Analysis for Synchronous Languages. - Frédéric Besson; Thomas P. Jensen; Jean-Pierre Talpin (SAS, 1999)

Verification of Control Flow based Security Properties. - Thomas P. Jensen; Daniel Le Métayer; Tommy Thorn (S&P, 1999)

An Operational Semantics of the Java Card Firewall. - Marc Éluard; Thomas P. Jensen; Ewen Denney (E-smart, 2001)

Class Analysis of Object-Oriented Programs through Abstract Interpretation. - Thomas P. Jensen; Fausto Spoto (FoSSaCS, 2001)

Model Checking Security Properties of Control Flow Graphs. - Frédéric Besson; Thomas P. Jensen; Daniel Le Métayer (J. Comput. Secur., 2001)

Types in Program Analysis. - Thomas P. Jensen (The Essence of Computation, 2002)

Secure Object Flow Analysis for Java Card. - Marc Éluard; Thomas P. Jensen (CARDIS, 2002)

Iteration schemes for fixed point calculation. - Thomas P. Jensen; Florimond Ployette; Olivier Ridoux (FICS, 2002)

Secure calling contexts for stack inspection. - Frédéric Besson; Thomas de Grenier de Latour; Thomas P. Jensen (PPDP, 2002)

Correctness of Java card method lookup via logical relations. - Ewen Denney; Thomas P. Jensen (Theor. Comput. Sci., 2002)

Modular Class Analysis with DATALOG. - Frédéric Besson; Thomas P. Jensen (SAS, 2003)

A Java Card CAP converter in PVS. - Thomas Genet; Thomas P. Jensen; Vikash Kodati; David Pichardie (COCV@ETAPS, 2003)

Modular Control-Flow Analysis with Rank 2 Intersection Types. - Anindya Banerjee 001; Thomas P. Jensen (Math. Struct. Comput. Sci., 2003)

Class analyses as abstract interpretations of trace semantics. - Fausto Spoto; Thomas P. Jensen (ACM Trans. Program. Lang. Syst., 2003)

Guest editors' introduction: Special issue on Formal Methods for Smart Cards. - Marieke Huisman; Thomas P. Jensen (J. Log. Algebraic Methods Program., 2004)

Validation du contrôle d'accès dans des cartes à puce multiapplications. - Marc Éluard; Thomas P. Jensen (Tech. Sci. Informatiques, 2004)

Certified Memory Usage Analysis. - David Cachera; Thomas P. Jensen; David Pichardie; Gerardo Schneider (FM, 2005)

Interfaces for stack inspection. - Frédéric Besson; Thomas de Grenier de Latour; Thomas P. Jensen (J. Funct. Program., 2005)

Extracting a data flow analyser in constructive logic. - David Cachera; Thomas P. Jensen; David Pichardie; Vlad Rusu (Theor. Comput. Sci., 2005)

Automata-Based Confidentiality Monitoring. - Gurvan Le Guernic; Anindya Banerjee 001; Thomas P. Jensen; David A. Schmidt (ASIAN, 2006)

A Formal Model of Access Control for Mobile Interactive Devices. - Frédéric Besson; Guillaume Dufay; Thomas P. Jensen (ESORICS, 2006)

Certificates of Resource Usage on Mobile Telephones. - Thomas P. Jensen (ISoLA, 2006)

Quantitative Static Analysis Over Semirings: Analysing Cache Behaviour for Java Card. - Pascal Sotin; David Cachera; Thomas P. Jensen (QAPL, 2006)

Proof-carrying code from certified abstract interpretation and fixpoint compression. - Frédéric Besson; Thomas P. Jensen; David Pichardie (Theor. Comput. Sci., 2006)

Small Witnesses for Abstract Interpretation-Based Proofs. - Frédéric Besson; Thomas P. Jensen; Tiphaine Turpin (ESOP, 2007)

The MOBIUS Proof Carrying Code Infrastructure. - Gilles Barthe; Pierre Crégut; Benjamin Grégoire; Thomas P. Jensen; David Pichardie (FMCO, 2007)

Rewriting Approximations for Fast Prototyping of Static Analyzers. - Yohan Boichut; Thomas Genet; Thomas P. Jensen; Luka Le Roux (RTA, 2007)

Certifying a Tree Automata Completion Checker. - Benoît Boyer; Thomas Genet; Thomas P. Jensen (IJCAR, 2008)

Computing Stack Maps with Interfaces. - Frédéric Besson; Thomas P. Jensen; Tiphaine Turpin (ECOOP, 2008)

Semantic Foundations and Inference of Non-null Annotations. - Laurent Hubert; Thomas P. Jensen; David Pichardie (FMOODS, 2008)

A Calculational Approach to Control-Flow Analysis by Abstract Interpretation. - Jan Midtgaard; Thomas P. Jensen (SAS, 2008)

Certified Static Analysis by Abstract Interpretation. - Frédéric Besson; David Cachera; Thomas P. Jensen; David Pichardie (FOSAD, 2009)

A Provably Correct Stackless Intermediate Representation for Java Bytecode. - Delphine Demange; Thomas P. Jensen; David Pichardie (APLAS, 2010)

Enforcing Secure Object Initialization in Java. - Laurent Hubert; Thomas P. Jensen; Vincent Monfort; David Pichardie (ESORICS, 2010)

Sawja: Static Analysis Workshop for Java. - Laurent Hubert; Nicolas Barré; Frédéric Besson; Delphine Demange; Thomas P. Jensen; Vincent Monfort; David Pichardie; Tiphaine Turpin (FoVeOOS, 2010)

Certified Result Checking for Polyhedral Analysis of Bytecode Programs. - Frédéric Besson; Thomas P. Jensen; David Pichardie; Tiphaine Turpin (TGC, 2010)

Verifying resource access control on mobile interactive devices. - Frédéric Besson; Guillaume Dufay; Thomas P. Jensen; David Pichardie (J. Comput. Secur., 2010)

Long-run cost analysis by approximation of linear operators over dioids. - David Cachera; Thomas P. Jensen; Arnaud Jobin; Pascal Sotin (Math. Struct. Comput. Sci., 2010)

Secure the Clones - Static Enforcement of Policies for Secure Object Copying. - Thomas P. Jensen; Florent Kirchner; David Pichardie (ESOP, 2011)

Secure the Clones - Thomas P. Jensen; Florent Kirchner; David Pichardie (Log. Methods Comput. Sci., 2012)

Control-flow analysis of function calls and returns by abstract interpretation. - Jan Midtgaard; Thomas P. Jensen (Inf. Comput., 2012)

Hybrid Information Flow Monitoring against Web Tracking. - Frédéric Besson; Nataliia Bielova; Thomas P. Jensen (CSF, 2013)

Result Certification of Static Program Analysers with Automated Theorem Provers. - Frédéric Besson; Pierre-Emmanuel Cornilleau; Thomas P. Jensen (VSTTE, 2013)

Pretty-big-step-semantics-based Certified Abstract Interpretation (Preliminary version). - Martin Bodin; Thomas P. Jensen; Alan Schmitt (Festschrift for Dave Schmidt, 2013)

Pretty-big-step-semantics-based Certified Abstract Interpretation. - Martin Bodin; Thomas P. Jensen; Alan Schmitt (JFLA, 2014)

Browser Randomisation against Fingerprinting: A Quantitative Information Flow Approach. - Frédéric Besson; Nataliia Bielova; Thomas P. Jensen (NordSec, 2014)

SawjaCard: A Static Analysis Tool for Certifying Java Card Applications. - Frédéric Besson; Thomas P. Jensen; Pierre Vittet (SAS, 2014)

Inference of polynomial invariants for imperative programs: A farewell to Gröbner bases. - David Cachera; Thomas P. Jensen; Arnaud Jobin; Florent Kirchner (Sci. Comput. Program., 2014)

Certified Abstract Interpretation with Pretty-Big-Step Semantics. - Martin Bodin; Thomas P. Jensen; Alan Schmitt (CPP, 2015)

Dependency Analysis of Functional Specifications with Algebraic Data Structures. - Oana Fabiana Andreescu; Thomas P. Jensen; Stéphane Lescuyer (ICFEM, 2015)

Hybrid Typing of Secure Information Flow in a JavaScript-Like Language. - José Fragoso Santos; Thomas P. Jensen; Tamara Rezk; Alan Schmitt (TGC, 2015)

Hybrid Monitoring of Attacker Knowledge. - Frédéric Besson; Nataliia Bielova; Thomas P. Jensen (CSF, 2016)

Correlating Structured Inputs and Outputs in Functional Specifications. - Oana Fabiana Andreescu; Thomas P. Jensen; Stéphane Lescuyer (SEFM, 2016)

Using JavaScript Monitoring to Prevent Device Fingerprinting. - Nataliia Bielova; Frédéric Besson; Thomas P. Jensen (ERCIM News, 2016)

Securing Compilation Against Memory Probing. - Frédéric Besson; Alexandre Dang; Thomas P. Jensen (PLAS@CCS, 2018)

Verifying Higher-Order Functions with Tree Automata. - Thomas Genet; Timothée Haudebourg; Thomas P. Jensen (FoSSaCS, 2018)

Verification of high-level transformations with inductive refinement types. - Ahmad Salim Al-Sibahi; Thomas P. Jensen; Aleksandar S. Dimovski; Andrzej Wasowski (GPCE, 2018)

Modular Software Fault Isolation as Abstract Interpretation. - Frédéric Besson; Thomas P. Jensen; Julien Lepiller (SAS, 2018)

Information-Flow Preservation in Compiler Optimisations. - Frédéric Besson; Alexandre Dang; Thomas P. Jensen (CSF, 2019)

Compiling Sandboxes: Formally Verified Software Fault Isolation. - Frédéric Besson; Sandrine Blazy; Alexandre Dang; Thomas P. Jensen; Pierre Wilke (ESOP, 2019)

Inferring frame conditions with static correlation analysis. - Oana Fabiana Andreescu; Thomas P. Jensen; Stéphane Lescuyer; Benoît Montagu (Proc. ACM Program. Lang., 2019)

Skeletal semantics and their interpretations. - Martin Bodin; Philippa Gardner; Thomas P. Jensen; Alan Schmitt (Proc. ACM Program. Lang., 2019)

Galois Connections for Recursive Types. - Ahmad Salim Al-Sibahi; Thomas P. Jensen; Rasmus Ejlers Møgelberg; Andrzej Wasowski (From Lambda Calculus to Cybersecurity Through Program Analysis, 2020)

Termination of Ethereum's Smart Contracts. - Thomas Genet; Thomas P. Jensen; Justine Sauvage (ICETE (2), 2020)

Numeric domains meet algebraic data types. - Santiago Bautista; Thomas P. Jensen; Benoît Montagu (NSAD@SAS, 2020)

Regular language type inference with term rewriting. - Timothée Haudebourg; Thomas Genet; Thomas P. Jensen (Proc. ACM Program. Lang., 2020)

Stable relations and abstract interpretation of higher-order programs. - Benoît Montagu; Thomas P. Jensen (Proc. ACM Program. Lang., 2020)

Trace-based control-flow analysis. - Benoît Montagu; Thomas P. Jensen (PLDI, 2021)

Verification of Program Transformations with Inductive Refinement Types. - Ahmad Salim Al-Sibahi; Thomas P. Jensen; Aleksandar S. Dimovski; Andrzej Wasowski (ACM Trans. Softw. Eng. Methodol., 2021)

Lifting Numeric Relational Domains to Algebraic Data Types. - Santiago Bautista; Thomas P. Jensen; Benoît Montagu (SAS, 2022)

Automata-Based Verification of Relational Properties of Functions over Algebraic Data Structures. - Théo Losekoot; Thomas Genet; Thomas P. Jensen (FSCD, 2023)

MichelsonLiSA: A Static Analyzer for Tezos. - Luca Olivieri; Thomas P. Jensen; Luca Negrini 001; Fausto Spoto (PerCom Workshops, 2023)

Type-directed Program Transformation for Constant-Time Enforcement. - Gautier Raimondi; Frédéric Besson; Thomas P. Jensen (PPDP, 2023)

Deriving Abstract Interpreters from Skeletal Semantics. - Thomas P. Jensen; Vincent Rebiscoul; Alan Schmitt (EXPRESS/SOS, 2023)

Verification of Programs with ADTs Using Shallow Horn Clauses. - Théo Losekoot; Thomas Genet; Thomas P. Jensen (SAS, 2024)

Axiomatising an information flow logic based on partial equivalence relations. - Andrzej Filinski; Ken Friis Larsen; Thomas P. Jensen (Int. J. Softw. Tools Technol. Transf., 2024)

An input-output relational domain for algebraic data types and functional arrays. - Santiago Bautista; Thomas P. Jensen; Benoît Montagu (Formal Methods Syst. Des., 2025)

Design and Implementation of Static Analyses for Tezos Smart Contracts. - Luca Olivieri; Luca Negrini 001; Vincenzo Arceri; Thomas P. Jensen; Fausto Spoto (Distributed Ledger Technol. Res. Pract., 2025)