| 2026 | ESOP | Complete Abstractions for Verification of Polymorphic Functions with Equality. | Malo Revel, Thomas Genet, Thomas P. Jensen |
| 2025 | SAS | Contextual Equality Saturation. | Alexandre Drewery, Thomas P. Jensen, David Pichardie |
| 2024 | SAS | Verification of Programs with ADTs Using Shallow Horn Clauses. | Tho Losekoot, Thomas Genet, Thomas P. Jensen |
| 2023 | FSCD | Automata-Based Verification of Relational Properties of Functions over Algebraic Data Structures. | Tho Losekoot, Thomas Genet, Thomas P. Jensen |
| 2023 | PERCOM | MichelsonLiSA: A Static Analyzer for Tezos. | Luca Olivieri, Thomas P. Jensen, Luca Negrini, Fausto Spoto |
| 2023 | PPDP | Type-directed Program Transformation for Constant-Time Enforcement. | Gautier Raimondi, Frdric Besson, Thomas P. Jensen |
| 2022 | SAS | Lifting Numeric Relational Domains to Algebraic Data Types. | Santiago Bautista, Thomas P. Jensen, Benot Montagu |
| 2021 | PLDI | Trace-based control-flow analysis. | Benot Montagu, Thomas P. Jensen |
| 2019 | ESOP | Compiling Sandboxes: Formally Verified Software Fault Isolation. | Frdric Besson, Sandrine Blazy, Alexandre Dang, Thomas P. Jensen, Pierre Wilke |
| 2018 | CCS | Securing Compilation Against Memory Probing. | Frdric Besson, Alexandre Dang, Thomas P. Jensen |
| 2018 | FOSSACS | Verifying Higher-Order Functions with Tree Automata. | Thomas Genet, Timothe Haudebourg, Thomas P. Jensen |
| 2018 | GPCE | Verification of high-level transformations with inductive refinement types. | Ahmad Salim Al-Sibahi, Thomas P. Jensen, Aleksandar S. Dimovski, Andrzej Wasowski |
| 2018 | SAS | Modular Software Fault Isolation as Abstract Interpretation. | Frdric Besson, Thomas P. Jensen, Julien Lepiller |
| 2016 | SEFM | Correlating Structured Inputs and Outputs in Functional Specifications. | Oana Fabiana Andreescu, Thomas P. Jensen, Stphane Lescuyer |
| 2015 | CPP | Certified Abstract Interpretation with Pretty-Big-Step Semantics. | Martin Bodin, Thomas P. Jensen, Alan Schmitt |
| 2015 | ICFEM | Dependency Analysis of Functional Specifications with Algebraic Data Structures. | Oana Fabiana Andreescu, Thomas P. Jensen, Stphane Lescuyer |
| 2014 | SAS | SawjaCard: A Static Analysis Tool for Certifying Java Card Applications. | Frdric Besson, Thomas P. Jensen, Pierre Vittet |
| 2012 | SAS | Inference of Polynomial Invariants for Imperative Programs: A Farewell to Grbner Bases. | David Cachera, Thomas P. Jensen, Arnaud Jobin, Florent Kirchner |
| 2011 | ESOP | Secure the Clones - Static Enforcement of Policies for Secure Object Copying. | Thomas P. Jensen, Florent Kirchner, David Pichardie |
| 2010 | APLAS | A Provably Correct Stackless Intermediate Representation for Java Bytecode. | Delphine Demange, Thomas P. Jensen, David Pichardie |
| 2010 | ESORICS | Enforcing Secure Object Initialization in Java. | Laurent Hubert, Thomas P. Jensen, Vincent Monfort, David Pichardie |
| 2009 | ICFP | Control-flow analysis of function calls and returns by abstract interpretation. | Jan Midtgaard, Thomas P. Jensen |
| 2008 | CADE | Certifying a Tree Automata Completion Checker. | Benot Boyer, Thomas Genet, Thomas P. Jensen |
| 2008 | ECOOP | Computing Stack Maps with Interfaces. | Frdric Besson, Thomas P. Jensen, Tiphaine Turpin |
| 2008 | SAS | A Calculational Approach to Control-Flow Analysis by Abstract Interpretation. | Jan Midtgaard, Thomas P. Jensen |
| 2007 | ESOP | Small Witnesses for Abstract Interpretation-Based Proofs. | Frdric Besson, Thomas P. Jensen, Tiphaine Turpin |
| 2006 | ESORICS | A Formal Model of Access Control for Mobile Interactive Devices. | Frdric Besson, Guillaume Dufay, Thomas P. Jensen |
| 2006 | ISoLA | Certificates of Resource Usage on Mobile Telephones. | Thomas P. Jensen |
| 2005 | FM | Certified Memory Usage Analysis. | David Cachera, Thomas P. Jensen, David Pichardie, Gerardo Schneider |
| 2004 | ESOP | Extracting a Data Flow Analyser in Constructive Logic. | David Cachera, Thomas P. Jensen, David Pichardie, Vlad Rusu |
| 2003 | SAS | Modular Class Analysis with DATALOG. | Frdric Besson, Thomas P. Jensen |
| 2002 | CARDIS | Secure Object Flow Analysis for Java Card. | Marc luard, Thomas P. Jensen |
| 2002 | PPDP | Secure calling contexts for stack inspection. | Frdric Besson, Thomas de Grenier de Latour, Thomas P. Jensen |
| 2001 | FOSSACS | Class Analysis of Object-Oriented Programs through Abstract Interpretation. | Thomas P. Jensen, Fausto Spoto |
| 2000 | ESOP | Correctness of Java Card Method Lookup via Logical Relations. | Ewen Denney, Thomas P. Jensen |
| 1999 | SP | Verification of Control Flow based Security Properties. | Thomas P. Jensen, Daniel Le Mtayer, Tommy Thorn |
| 1999 | SAS | Polyhedral Analysis for Synchronous Languages. | Frdric Besson, Thomas P. Jensen, Jean-Pierre Talpin |
| 1998 | POPL | Inference of Polymorphic and Conditional Strictness Properties. | Thomas P. Jensen |
| 1996 | ESOP | Flow Analysis in the Geometry of Interaction. | Thomas P. Jensen, Ian Mackie |
| 1995 | PEPM | Clock Analysis of Synchronous Dataflow Programs. | Thomas P. Jensen |
| 1993 | SAS | A Congruence for Gamma Programs. | Lindsay Errington, Chris Hankin, Thomas P. Jensen |
| 1992 | CONCUR | Homology of Higher Dimensional Automata. | Eric Goubault, Thomas P. Jensen |
| 1992 | LICS | Disjunctive Strictness Analysis | Thomas P. Jensen |
| 1992 | SAS | Axiomatising Uniform Properties of Recursive Data Structures. | Thomas P. Jensen |
| 1991 | POPL | A Relational Approach to Strictness Analysis for Higher-Order Polymorphic Functions. | Samson Abramsky, Thomas P. Jensen |
| 1990 | ESOP | A Backwards Analysis for Compile-time Garbage Collection. | Thomas P. Jensen, Torben . Mogensen |