Thomas P. Jensen

112 papers A* 4A 16B 20C 6Journal 29Unranked 34

Year	Rank	Type	Title / Venue / Authors
2026	—	`conf`	Complete Abstractions for Verification of Polymorphic Functions with Equality. ESOP (2) Malo Revel, Thomas Genet, Thomas P. Jensen
2026	B	`ed.`	Verification, Model Checking, and Abstract Interpretation - 27th International Conference, VMCAI 2026, Rennes, France, January 12-13, 2026, Proceedings VMCAI Yu-Fang Chen, Thomas P. Jensen, Ondrej Lengál
2025	J	`jnl`	An input-output relational domain for algebraic data types and functional arrays. Formal Methods Syst. Des. Santiago Bautista, Thomas P. Jensen, Benoît Montagu
2025	B	`conf`	Contextual Equality Saturation. SAS Alexandre Drewery, Thomas P. Jensen, David Pichardie
2025	J	`jnl`	Design and Implementation of Static Analyses for Tezos Smart Contracts. Distributed Ledger Technol. Res. Pract. Luca Olivieri, Luca Negrini, Vincenzo Arceri, Thomas P. Jensen, Fausto Spoto
2024	J	`jnl`	Axiomatising an information flow logic based on partial equivalence relations. Int. J. Softw. Tools Technol. Transf. Andrzej Filinski, Ken Friis Larsen, Thomas P. Jensen
2024	B	`conf`	Verification of Programs with ADTs Using Shallow Horn Clauses. SAS Théo Losekoot, Thomas Genet, Thomas P. Jensen
2023	B	`conf`	Automata-Based Verification of Relational Properties of Functions over Algebraic Data Structures. FSCD Théo Losekoot, Thomas Genet, Thomas P. Jensen
2023	—	`conf`	Deriving Abstract Interpreters from Skeletal Semantics. EXPRESS/SOS Thomas P. Jensen, Vincent Rebiscoul, Alan Schmitt
2023	—	`conf`	MichelsonLiSA: A Static Analyzer for Tezos. PerCom Workshops Luca Olivieri, Thomas P. Jensen, Luca Negrini, Fausto Spoto
2023	C	`conf`	Type-directed Program Transformation for Constant-Time Enforcement. PPDP Gautier Raimondi, Frédéric Besson, Thomas P. Jensen
2022	B	`conf`	Lifting Numeric Relational Domains to Algebraic Data Types. SAS Santiago Bautista, Thomas P. Jensen, Benoît Montagu
2021	A*	`conf`	Trace-based control-flow analysis. PLDI Benoît Montagu, Thomas P. Jensen
2021	J	`jnl`	Verification of Program Transformations with Inductive Refinement Types. ACM Trans. Softw. Eng. Methodol. Ahmad Salim Al-Sibahi, Thomas P. Jensen, Aleksandar S. Dimovski, Andrzej Wasowski
2020	—	`conf`	Galois Connections for Recursive Types. From Lambda Calculus to Cybersecurity Through Program Analysis Ahmad Salim Al-Sibahi, Thomas P. Jensen, Rasmus Ejlers Møgelberg, Andrzej Wasowski
2020	—	`conf`	Numeric domains meet algebraic data types. NSAD@SAS Santiago Bautista, Thomas P. Jensen, Benoît Montagu
2020	J	`jnl`	Regular language type inference with term rewriting. Proc. ACM Program. Lang. Timothée Haudebourg, Thomas Genet, Thomas P. Jensen
2020	J	`jnl`	Stable relations and abstract interpretation of higher-order programs. Proc. ACM Program. Lang. Benoît Montagu, Thomas P. Jensen
2020	—	`conf`	Termination of Ethereum's Smart Contracts. ICETE (2) Thomas Genet, Thomas P. Jensen, Justine Sauvage
2019	A	`conf`	Compiling Sandboxes: Formally Verified Software Fault Isolation. ESOP Frédéric Besson, Sandrine Blazy, Alexandre Dang, Thomas P. Jensen, Pierre Wilke
2019	J	`jnl`	Inferring frame conditions with static correlation analysis. Proc. ACM Program. Lang. Oana Fabiana Andreescu, Thomas P. Jensen, Stéphane Lescuyer, Benoît Montagu
2019	A	`conf`	Information-Flow Preservation in Compiler Optimisations. CSF Frédéric Besson, Alexandre Dang, Thomas P. Jensen
2019	J	`jnl`	Skeletal semantics and their interpretations. Proc. ACM Program. Lang. Martin Bodin, Philippa Gardner, Thomas P. Jensen, Alan Schmitt
2018	B	`conf`	Modular Software Fault Isolation as Abstract Interpretation. SAS Frédéric Besson, Thomas P. Jensen, Julien Lepiller
2018	—	`conf`	Securing Compilation Against Memory Probing. PLAS@CCS Frédéric Besson, Alexandre Dang, Thomas P. Jensen
2018	J	`jnl`	Skeletal Semantics and their Interpretations. CoRR Martin Bodin, Philippa Gardner, Thomas P. Jensen, Alan Schmitt
2018	J	`jnl`	Verification of High-Level Transformations with Inductive Refinement Types. CoRR Ahmad Salim Al-Sibahi, Thomas P. Jensen, Aleksandar S. Dimovski, Andrzej Wasowski
2018	B	`conf`	Verification of high-level transformations with inductive refinement types. GPCE Ahmad Salim Al-Sibahi, Thomas P. Jensen, Aleksandar S. Dimovski, Andrzej Wasowski
2018	B	`conf`	Verifying Higher-Order Functions with Tree Automata. FoSSaCS Thomas Genet, Timothée Haudebourg, Thomas P. Jensen
2016	B	`conf`	Correlating Structured Inputs and Outputs in Functional Specifications. SEFM Oana Fabiana Andreescu, Thomas P. Jensen, Stéphane Lescuyer
2016	A	`conf`	Hybrid Monitoring of Attacker Knowledge. CSF Frédéric Besson, Nataliia Bielova, Thomas P. Jensen
2016	J	`jnl`	Using JavaScript Monitoring to Prevent Device Fingerprinting. ERCIM News Nataliia Bielova, Frédéric Besson, Thomas P. Jensen
2015	B	`conf`	Certified Abstract Interpretation with Pretty-Big-Step Semantics. CPP Martin Bodin, Thomas P. Jensen, Alan Schmitt
2015	C	`conf`	Dependency Analysis of Functional Specifications with Algebraic Data Structures. ICFEM Oana Fabiana Andreescu, Thomas P. Jensen, Stéphane Lescuyer
2015	—	`conf`	Hybrid Typing of Secure Information Flow in a JavaScript-Like Language. TGC José Fragoso Santos, Thomas P. Jensen, Tamara Rezk, Alan Schmitt
2015	B	`ed.`	Static Analysis - 22nd International Symposium, SAS 2015, Saint-Malo, France, September 9-11, 2015, Proceedings SAS Sandrine Blazy, Thomas P. Jensen
2014	—	`conf`	Browser Randomisation against Fingerprinting: A Quantitative Information Flow Approach. NordSec Frédéric Besson, Nataliia Bielova, Thomas P. Jensen
2014	J	`jnl`	Inference of polynomial invariants for imperative programs: A farewell to Gröbner bases. Sci. Comput. Program. David Cachera, Thomas P. Jensen, Arnaud Jobin, Florent Kirchner
2014	—	`conf`	Pretty-big-step-semantics-based Certified Abstract Interpretation. JFLA Martin Bodin, Thomas P. Jensen, Alan Schmitt
2014	B	`conf`	SawjaCard: A Static Analysis Tool for Certifying Java Card Applications. SAS Frédéric Besson, Thomas P. Jensen, Pierre Vittet
2013	A	`conf`	Hybrid Information Flow Monitoring against Web Tracking. CSF Frédéric Besson, Nataliia Bielova, Thomas P. Jensen
2013	—	`conf`	Pretty-big-step-semantics-based Certified Abstract Interpretation (Preliminary version). Festschrift for Dave Schmidt Martin Bodin, Thomas P. Jensen, Alan Schmitt
2013	—	`conf`	Result Certification of Static Program Analysers with Automated Theorem Provers. VSTTE Frédéric Besson, Pierre-Emmanuel Cornilleau, Thomas P. Jensen
2012	J	`jnl`	Control-flow analysis of function calls and returns by abstract interpretation. Inf. Comput. Jan Midtgaard, Thomas P. Jensen
2012	B	`conf`	Inference of Polynomial Invariants for Imperative Programs: A Farewell to Gröbner Bases. SAS David Cachera, Thomas P. Jensen, Arnaud Jobin, Florent Kirchner
2012	J	`jnl`	Secure the Clones Log. Methods Comput. Sci. Thomas P. Jensen, Florent Kirchner, David Pichardie
2011	A	`conf`	Secure the Clones - Static Enforcement of Policies for Secure Object Copying. ESOP Thomas P. Jensen, Florent Kirchner, David Pichardie
2010	B	`conf`	A Provably Correct Stackless Intermediate Representation for Java Bytecode. APLAS Delphine Demange, Thomas P. Jensen, David Pichardie
2010	—	`conf`	Certified Result Checking for Polyhedral Analysis of Bytecode Programs. TGC Frédéric Besson, Thomas P. Jensen, David Pichardie, Tiphaine Turpin
2010	J	`jnl`	Enforcing Secure Object Initialization in Java CoRR Laurent Hubert, Thomas P. Jensen, Vincent Monfort, David Pichardie
2010	A	`conf`	Enforcing Secure Object Initialization in Java. ESORICS Laurent Hubert, Thomas P. Jensen, Vincent Monfort, David Pichardie
2010	J	`jnl`	Long-run cost analysis by approximation of linear operators over dioids. Math. Struct. Comput. Sci. David Cachera, Thomas P. Jensen, Arnaud Jobin, Pascal Sotin
2010	J	`jnl`	Sawja: Static Analysis Workshop for Java CoRR Laurent Hubert, Nicolas Barré, Frédéric Besson, Delphine Demange, Thomas P. Jensen, Vincent Monfort, David Pichardie, Tiphaine Turpin
2010	—	`conf`	Sawja: Static Analysis Workshop for Java. FoVeOOS Laurent Hubert, Nicolas Barré, Frédéric Besson, Delphine Demange, Thomas P. Jensen, Vincent Monfort, David Pichardie, Tiphaine Turpin
2010	J	`jnl`	Verifying resource access control on mobile interactive devices. J. Comput. Secur. Frédéric Besson, Guillaume Dufay, Thomas P. Jensen, David Pichardie
2009	—	`conf`	Certified Static Analysis by Abstract Interpretation. FOSAD Frédéric Besson, David Cachera, Thomas P. Jensen, David Pichardie
2009	A	`conf`	Control-flow analysis of function calls and returns by abstract interpretation. ICFP Jan Midtgaard, Thomas P. Jensen
2008	B	`conf`	A Calculational Approach to Control-Flow Analysis by Abstract Interpretation. SAS Jan Midtgaard, Thomas P. Jensen
2008	A	`conf`	Certifying a Tree Automata Completion Checker. IJCAR Benoît Boyer, Thomas Genet, Thomas P. Jensen
2008	A	`conf`	Computing Stack Maps with Interfaces. ECOOP Frédéric Besson, Thomas P. Jensen, Tiphaine Turpin
2008	—	`conf`	Long-Run Cost Analysis by Approximation of Linear Operators over Dioids. AMAST David Cachera, Thomas P. Jensen, Arnaud Jobin, Pascal Sotin
2008	—	`conf`	Semantic Foundations and Inference of Non-null Annotations. FMOODS Laurent Hubert, Thomas P. Jensen, David Pichardie
2007	—	`conf`	Rewriting Approximations for Fast Prototyping of Static Analyzers. RTA Yohan Boichut, Thomas Genet, Thomas P. Jensen, Luka Le Roux
2007	A	`conf`	Small Witnesses for Abstract Interpretation-Based Proofs. ESOP Frédéric Besson, Thomas P. Jensen, Tiphaine Turpin
2007	—	`conf`	The MOBIUS Proof Carrying Code Infrastructure. FMCO Gilles Barthe, Pierre Crégut, Benjamin Grégoire, Thomas P. Jensen, David Pichardie
2006	A	`conf`	A Formal Model of Access Control for Mobile Interactive Devices. ESORICS Frédéric Besson, Guillaume Dufay, Thomas P. Jensen
2006	—	`conf`	Automata-Based Confidentiality Monitoring. ASIAN Gurvan Le Guernic, Anindya Banerjee, Thomas P. Jensen, David A. Schmidt
2006	C	`conf`	Certificates of Resource Usage on Mobile Telephones. ISoLA Thomas P. Jensen
2006	J	`jnl`	Proof-carrying code from certified abstract interpretation and fixpoint compression. Theor. Comput. Sci. Frédéric Besson, Thomas P. Jensen, David Pichardie
2006	—	`conf`	Quantitative Static Analysis Over Semirings: Analysing Cache Behaviour for Java Card. QAPL Pascal Sotin, David Cachera, Thomas P. Jensen
2005	B	`conf`	Certified Memory Usage Analysis. FM David Cachera, Thomas P. Jensen, David Pichardie, Gerardo Schneider
2005	J	`jnl`	Extracting a data flow analyser in constructive logic. Theor. Comput. Sci. David Cachera, Thomas P. Jensen, David Pichardie, Vlad Rusu
2005	J	`jnl`	Interfaces for stack inspection. J. Funct. Program. Frédéric Besson, Thomas de Grenier de Latour, Thomas P. Jensen
2005	—	`ed.`	Proceedings of the 2005 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis For Software Tools and Engineering, PASTE'05, Lisbon, Portugal, September 5-6, 2005 PASTE Michael D. Ernst, Thomas P. Jensen
2004	A	`conf`	Extracting a Data Flow Analyser in Constructive Logic. ESOP David Cachera, Thomas P. Jensen, David Pichardie, Vlad Rusu
2004	J	`jnl`	Guest editors' introduction: Special issue on Formal Methods for Smart Cards. J. Log. Algebraic Methods Program. Marieke Huisman, Thomas P. Jensen
2004	J	`jnl`	Validation du contrôle d'accès dans des cartes à puce multiapplications. Tech. Sci. Informatiques Marc Éluard, Thomas P. Jensen
2003	—	`conf`	A Java Card CAP converter in PVS. COCV Thomas Genet, Thomas P. Jensen, Vikash Kodati, David Pichardie
2003	J	`jnl`	Class analyses as abstract interpretations of trace semantics. ACM Trans. Program. Lang. Syst. Fausto Spoto, Thomas P. Jensen
2003	B	`conf`	Modular Class Analysis with DATALOG. SAS Frédéric Besson, Thomas P. Jensen
2003	J	`jnl`	Modular Control-Flow Analysis with Rank 2 Intersection Types. Math. Struct. Comput. Sci. Anindya Banerjee, Thomas P. Jensen
2002	J	`jnl`	Correctness of Java card method lookup via logical relations. Theor. Comput. Sci. Ewen Denney, Thomas P. Jensen
2002	—	`conf`	Iteration schemes for fixed point calculation. FICS Thomas P. Jensen, Florimond Ployette, Olivier Ridoux
2002	C	`conf`	Secure Object Flow Analysis for Java Card. CARDIS Marc Éluard, Thomas P. Jensen
2002	C	`conf`	Secure calling contexts for stack inspection. PPDP Frédéric Besson, Thomas de Grenier de Latour, Thomas P. Jensen
2002	—	`conf`	Types in Program Analysis. The Essence of Computation Thomas P. Jensen
2001	—	`conf`	An Operational Semantics of the Java Card Firewall. E-smart Marc Éluard, Thomas P. Jensen, Ewen Denney
2001	B	`conf`	Class Analysis of Object-Oriented Programs through Abstract Interpretation. FoSSaCS Thomas P. Jensen, Fausto Spoto
2001	—	`ed.`	Java on Smart Cards: Programming and Security, First International Workshop, JavaCard 2000, Cannes, France, September 14, 2000, Revised Papers Java Card Isabelle Attali, Thomas P. Jensen
2001	J	`jnl`	Model Checking Security Properties of Control Flow Graphs. J. Comput. Secur. Frédéric Besson, Thomas P. Jensen, Daniel Le Métayer
2001	—	`ed.`	Smart Card Programming and Security, International Conference on Research in Smart Cards, E-smart 2001, Cannes, France, September 19-21, 2001, Proceedings E-smart Isabelle Attali, Thomas P. Jensen
2000	A	`conf`	Correctness of Java Card Method Lookup via Logical Relations. ESOP Ewen Denney, Thomas P. Jensen
1999	B	`conf`	Polyhedral Analysis for Synchronous Languages. SAS Frédéric Besson, Thomas P. Jensen, Jean-Pierre Talpin
1999	—	`conf`	Verification of Control Flow based Security Properties. S&P Thomas P. Jensen, Daniel Le Métayer, Tommy Thorn
1998	—	`conf`	Coarse Grained Java Security Policies. ECOOP Workshops Thomas P. Jensen, Daniel Le Métayer, Tommy Thorn
1998	A*	`conf`	Inference of Polymorphic and Conditional Strictness Properties. POPL Thomas P. Jensen
1998	—	`conf`	Security and Dynamic Class Loading in Java: A Formalization. ICCL Thomas P. Jensen, Daniel Le Métayer, Tommy Thorn
1997	J	`jnl`	Disjunctive Program Analysis for Algebraic Data Types. ACM Trans. Program. Lang. Syst. Thomas P. Jensen
1996	A	`conf`	Flow Analysis in the Geometry of Interaction. ESOP Thomas P. Jensen, Ian Mackie
1995	C	`conf`	Clock Analysis of Synchronous Dataflow Programs. PEPM Thomas P. Jensen
1995	J	`jnl`	Conjunctive Type Systems and Abstract Interpretation of Higher-Order Functional Programs. J. Log. Comput. Thomas P. Jensen
1994	—	`conf`	Abstract Interpretation over Algebraic Data Types. ICCL Thomas P. Jensen
1994	—	`conf`	Denotational Semantics of Timed Dataflow Programs. Theory and Formal Methods Thomas P. Jensen
1993	—	`conf`	A Congruence for Gamma Programs. WSA Lindsay Errington, Chris Hankin, Thomas P. Jensen
1993	—	`conf`	Reasoning About Gamma Programs. Theory and Formal Methods Lindsay Errington, Chris Hankin, Thomas P. Jensen
1992	—	`conf`	Axiomatising Uniform Properties of Recursive Data Structures. WSA Thomas P. Jensen
1992	A*	`conf`	Disjunctive Strictness Analysis LICS Thomas P. Jensen
1992	B	`conf`	Homology of Higher Dimensional Automata. CONCUR Eric Goubault, Thomas P. Jensen
1991	A*	`conf`	A Relational Approach to Strictness Analysis for Higher-Order Polymorphic Functions. POPL Samson Abramsky, Thomas P. Jensen
1991	—	`conf`	Strictness Analysis in Logical Form. FPCA Thomas P. Jensen
1990	A	`conf`	A Backwards Analysis for Compile-time Garbage Collection. ESOP Thomas P. Jensen, Torben Æ. Mogensen
1990	A	`conf`	Abstract Interpretation vs. Type Inference A Topological Perspective. Functional Programming Thomas P. Jensen