\paragraph{Books}
\begin{biblibook}
\nextbook{Huisman:04:JLAPSmartCards}  {\em J. Logic and Algebraic Programming. Special issue on Formal 		 Methods for Smart Cards, vol. 58(1-2)}, M. Huisman, T. Jensen (Eds), Elsevier, 2004.
\nextbook{Attali:01:EsmartProceedings}  Isabelle Attali, Thomas Jensen. {\em Smart Card Programming and Security (e-Smart 2001)}, Isabelle Attali, Thomas JensenIsabelle Attali, Thomas Jensen (Eds), Springer LNCS vol. 2140, September 2001.
\nextbook{Jensen:00:JavaCard}  {\em Proceedings of the International Workshop on Java Card 		 (Java Card 2000)}, I. Attali, T. Jensen (Eds), Inria, Cannes, France, September 2000.
\end{biblibook}
\paragraph{ Academic Journals}
\begin{biblijournal}
\nextjournal{CacJenJobSotMSCS}  David Cachera, Thomas Jensen, Arnaud Jobin, Pascal Sotin. Long-Run Cost Analysis by Approximation of Linear Operators over Dioids. {\em Mathematical Structures in Computer Science}, 20(4):589-624, 2010.
\nextjournal{JCS10:Besson:Jensen:Dufay:Pichardie}  Frédéric Besson, Thomas Jensen, Guillaume Dufay, David Pichardie. Verifying Resource Access Control on Mobile Interactive Devices. {\em Journal of Computer Security}, 18(6):971-998, 2010.
\nextjournal{genet:2010:inria-00495405:1}  Thomas Genet, Vlad Rusu. Equational Approximations for Tree Automata Completion. {\em Journal of Symbolic Computation}, 45(5):574-597, May 2010(5):574-597, 2010.
\nextjournal{Got}  A. Gotlieb. TCAS software verification using Constraint Programming. {\em The Knowledge Engineering Review}, {Under revision}, 2009.
\nextjournal{Blazy-Leroy-Clight-09}  Sandrine Blazy, Xavier Leroy. Mechanized semantics for the {Clight} subset of the {C} language. {\em Journal of Automated Reasoning}, 43(3):263-288, 2009.
\nextjournal{GDB07}  A. Gotlieb, T. Denmat, B. Botella. Goal-oriented test data generation for pointer programs. {\em Information and Software Technology}, 49(9):1030-1044,  2007.
\nextjournal{TCSAppSem:BessonJensenPichardie}  Frédéric Besson, Thomas Jensen, David Pichardie. Proof-Carrying Code from Certified Abstract Interpretation to Fixpoint Compression. {\em Theoretical Computer Science}, 364(3):273-291, 2006.
\nextjournal{BGM05}  B. Botella, A. Gotlieb, C. Michel. Symbolic execution of floating-point computations. {\em The Software Testing, Verification and Reliability journal}, {to appear}, 2006.
\nextjournal{Besson:05:Interfaces}  F. Besson, T. de Grenier de Latour, T. Jensen. Interfaces for stack inspection. {\em Journal of Functional Programming}, 15(2):179-217, 2005.
\nextjournal{CaJePiRu05TCSExtractAnalyser}  David Cachera, Thomas Jensen, David Pichardie, Vlad Rusu. {Extracting a Data Flow Analyser in Constructive Logic}. {\em Theoretical Computer Science}, 2005.
\nextjournal{CacMorTECS05}  David Cachera, Katell Morin-Allory. Verification of safety properties for parameterized regular systems. {\em Trans. on Embedded Computing Systems}, 4(2):228-266, 2005.
\nextjournal{Eluard:04:TSI}  M. Eluard, T. Jensen. Vérification du contrôle d'accès dans des cartes à puce 		 multi-application. {\em Technique et Science Informatiques}, 23(3):323-358, 2004.
\nextjournal{FeuilladeGVTT-JAR04}  G. Feuillade, T. Genet, V. Viet Triem Tong. {R}eachability {A}nalysis over {T}erm {R}ewriting {S}ystems. {\em Journal of Automated Reasoning}, 33 (3-4):341-383, 2004.
\nextjournal{Jensen:04:CartesAPuce}  T. Jensen, J.-L. Lanet. Modélisation et vérification dans les cartes à puce. {\em Revue d'électricité et de l'électronique}, 6/7:89-94, 2004.
\nextjournal{Banerjee:03:Rank2}  A. Banerjee, T. Jensen. Control-flow analysis with rank-2 intersection types. {\em Mathematical Structures in Computer Science}, 13(1):87-124, 2003.
\nextjournal{Spoto:ClassAnalysis:03}  F. Spoto, T. Jensen. {C}lass {A}nalyses as {A}bstract {I}nterpretations of {T}race {S}emantics. {\em ACM Transactions on Programming Languages and Systems (TOPLAS)}, 25(5):578-630, 2003.
\nextjournal{Denney:02:Correctness}  E. Denney, T. Jensen. Correctness of {J}ava {C}ard method lookup via logical relations. {\em Theoretical Computer Science}, 283:305-331, 2002.
\nextjournal{Besson:01:ModelChecking}  F. Besson, T. Jensen, D. Le Métayer, T. Thorn. Model ckecking security properties of control flow graphs. {\em Journal of Computer Security}, 9:217-250, 2001.
\nextjournal{Jensen:97:Disjunctive}  T. Jensen. Disjunctive Program Analysis for Algebraic Data Types. {\em {ACM} Transactions on Programming Languages and Systems}, 19(5):752-804, 1997.
\end{biblijournal}
\paragraph{Book Chapters}
\begin{bibliinbook}
\nextinbook{wscp/part7}  Benjamin Blanc, Arnaud Gotlieb, Claude Michel. Constraints in Software Testing, Verification and Analysis. In {\em Trends in Constraint Programming}, Fré Benhamou, Narendra Jussien, Barry O'Sullivan (eds.), Chap. 7, pp. 333-368, ISTE, London, UK, May 2007.
\nextinbook{Jensen:02:Types}  T. Jensen. Types in program analysis. In {\em The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones}, Torben Mogensen, David Schmidt, I. Hal Sudborough (eds.), pp. 204-222, Lecture Notes in Computer Science 2566, Springer-Verlag, 2002.
\end{bibliinbook}
\paragraph{International Conferences}
\begin{bibliconference}
\nextconference{CacJobQAPL10}  David Cachera, Arnaud Jobin. Injecting Abstract Interpretations into Linear Cost Models. In {\em 8th Workshop on Quantitative Aspects of Programming Languages (QAPL)}, EPTCS, Paphos, 2010.
\nextconference{APLAS10:Demange:Jensen:Pichardie}  Delphine Demange, Thomas Jensen, David Pichardie. A Provably Correct Stackless Intermediate Representation for {J}ava Bytecode. In {\em 8th Asian Symposium on Programming Languages and Systems (APLAS)}, Lecture Notes in Computer Science, Vol 6461, 2010.
\nextconference{ITP10:Cachera:Pichardie}  David Cachera, David Pichardie. A Certified Denotational Abstract Interpreter. In {\em Proc.\ of International Conference on Interactive Theorem Proving (ITP-10)}, Lecture Notes in Computer Science, Vol 6172, pp. 9-24, 2010.
\nextconference{TGC10:Besson:Jensen:Pichardie:Turpin}  Frédéric Besson, Thomas Jensen, David Pichardie, Tiphaine Turpin. Certified Result Checking for Polyhedral Analysis of Bytecode Programs. In {\em Proc.\ of the 5th International Symposium on Trustworthy Global Computing (TGC 2010)}, {To appear}, Lecture Notes in Computer Science, 2010.
\nextconference{hubert:2010:inria-00504047:1}  Laurent Hubert, Nicolas Barré, Frédéric Besson, Delphine Demange, Thomas Jensen, Vincent Monfort, David Pichardie, Tiphaine Turpin. Sawja: Static Analysis Workshop for Java. In {\em 1st International Conference on Formal Verification of Object-Oriented Software (FoVeOOS)}, Lecture Notes in Computer Science, 2010.
\nextconference{hubert:2010:inria-00503953:1}  Laurent Hubert, Thomas Jensen, Vincent Montfort, David Pichardie. Enforcing Secure Object Initialization in Java. In {\em 15th European Symposium on Research in Computer Security (ESORICS)}, Lecture Notes in Computer Science, Vol 6345, pp. 101-115, 2010.
\nextconference{kirchner:2010:inria-00494531:1}  Helene Kirchner, Kirchner Florent, Claude Kirchner. Constraint Based Strategies. In {\em 18th International Workshop on Functional and Constraint Logic Programming - WFLP 2009}, Vol 5979, pp. 13-26, Brésil Brasilia, 2010.
\nextconference{besson:2010:inria-00517308:1}  Frédéric Besson. On using an inexact floating-point LP solver for deciding linear arithmetic in an SMT solver. In {\em 8th International Workshop on Satisfiability Modulo Theories}, 2010.
\nextconference{blazy:2010:inria-00477689:1}  Sandrine Blazy, Benoît Robillard, Andrew W. Appel. Formal Verification of Coalescing Graph-Coloring Register Allocation. In {\em 19th European Symposium on Programming (ESOP)}, Vol 6012, pp. 145-164, Chypre Paphos, March 2010.
\nextconference{GLM10}  A. Gotlieb, M. Leconte, B. Marre. Constraint Solving on Modular Integers. In {\em Proc. of the 9th Int. Workshop on Constraint Modelling and Reformulation (ModRef'10), co-located with CP'2010}, St Andrews, Scotland,  2010.
\nextconference{LGL10b}  N. Lazaar, A. Gotlieb, Y. Lebbah. Fault Localization in Constraint Programs. In {\em 22th Int. Conf. on Tools with Artificial Intelligence (ICTAI'2010)}, Arras, France,  2010.
\nextconference{CG10}  F. Charreteur, A. Gotlieb. Constraint-Based Test Input Generation for Java Bytecode. In {\em Proc. of the 21st IEEE Int. Symp. on Softw. Reliability Engineering (ISSRE'10)}, San Jose, CA, USA,  2010.
\nextconference{LGL10a}  N. Lazaar, A. Gotlieb, Y. Lebbah. On Testing Constraint Programs. In {\em 16th Int. Conf. on Principles and Practices of Constraint Programming (CP'2010)}, St Andrews, Scotland,  2010.
\nextconference{CDG10}  M. Carlier, C. Dubois, A. Gotlieb. Constraint Reasonning in FOCALTEST. In {\em 5rd International Conference on Software and Data Technologies (ICSOFT'10)}, Athens, Greece,  2010.
\nextconference{DBG10}  M. Delahaye, B. Botella, A. Gotlieb. Explanation-based generalization of infeasible path. In {\em 3rd IEEE International Conference on Software Testing, Validation and Verification (ICST'10)}, Paris, France,  2010.
\nextconference{VNC2009}  Gilles Guette, Olivier Heen. A TPM-based Architecture for Improved Security and Anonymity in Vehicular Ad hoc Networks. In {\em In International Vehicular Networking Conference (IEEE VNC 2009)}, 2009.
\nextconference{WISTP2009}  Olivier Heen, Gilles Guette, Thomas Genet. On the Unobservability of a Trust Relation in Mobile Ad Hoc Networks. In {\em WISTP 2009 3rd edition}, LNCS, Vol 5746, 2009.
\nextconference{MidtgaardJ09}  Jan Midtgaard, Thomas Jensen. Control-flow analysis of function calls and returns by abstract interpretation. In {\em Proceedings of the 14th ACM international conference on Functional programming}, pp. 287-298, 2009.
\nextconference{Besson09}  Frédéric Besson. CPA beats oo-CFA. In {\em Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs}, pp. 1-6, 2009.
\nextconference{2009-Blazy-Robillard}  Sandrine Blazy, Benoît Robillard. Live-range Unsplitting for Faster Optimal Coalescing. In {\em Proceedings of the ACM SIGPLAN/SIGBED 2009 conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2009)}, pp. 70-79, 2009.
\nextconference{BoyerG-RULE09}  B. Boyer, T. Genet. Verifying {T}emporal {R}egular properties of {A}bstractions of {T}erm {R}ewriting {S}ystems. In {\em {P}roc. of RULE'09}, EPTCS, Vol 21, 2009.
\nextconference{TPHOLs09:Dabrowski:Pichardie}  Frédéric Dabrowski, David Pichardie. A Certified Data Race Analysis for a Java-like Language. In {\em Proc.\ of 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs'09)}, Lecture Notes in Computer Science, Vol 5674, pp. 212-227, 2009.
\nextconference{NFM09:Cachera:Pichardie}  David Cachera, David Pichardie. Comparing Techniques for Certified Static Analysis. In {\em Proc.\ of the 1st NASA Formal Methods Symposium (NFM'09)}, pp. 111-115, 2009.
\nextconference{BYTECODE09:Hubert:Pichardie}  Laurent Hubert, David Pichardie. Soundly Handling Static Fields: Issues, Semantics and Analysis. In {\em Proc.\ of the 4th International Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE'09)}, Electronic Notes in Theoretical Computer Science, Vol 253, pp. 15-30, 2009.
\nextconference{LGL08}  N. Lazaar, A. Gotlieb, Y. Lebbah. Towards Constraint-Based Local Search for Automatic Test Data Generation. In {\em 1th International Workshop on Search-based Test Data Generation, co-located with ICST 2009}, Lillehammer, Norway,  2009.
\nextconference{Got09}  A. Gotlieb. EUCLIDE: A Constraint-Based Testing platform for critical C programs. In {\em 2th International Conference on Software Testing, Validation and Verification (ICST'09)}, Denver, CO,  2009.
\nextconference{GP09}  A. Gotlieb, M. Petit. Towards a Theory for Testing Non-terminating Programs. In {\em 33nd Annual IEEE International Computer Software and Applications Conference (COMPSAC'09)}, {6 pages}, Seattle, USA,  2009.
\nextconference{Besson-Jensen-Turpin:ECOOP08}  Frédéric Besson, Thomas Jensen, T. Turpin. Computing stack maps with interfaces. In {\em Proc. of the 22nd European Conference on Object-Oriented Programming (ECOOP 2008)}, LNCS, Vol 5142, pp. 642-666, 2008.
\nextconference{Midtgaard-Jensen:SAS08}  J. Midtgaard, Thomas Jensen. A Calculational Approach to Control-Flow Analysis by Abstract Interpretation. In {\em Static Analysis, 15th International Symposium, SAS 2008}, Lectures Notes in Computer Science, Vol 5079, pp. 347-362, 2008.
\nextconference{BoyerGJ-IJCAR08}  B. Boyer, Thomas Genet, Thomas Jensen. {C}ertifying a {T}ree {A}utomata {C}ompletion {C}hecker. In {\em 4th International Joint Conference, IJCAR 2008}, Lectures Notes in Computer Science, Vol 5195, pp. 347-362, 2008.
\nextconference{HeenGGP-MWNS08}  Olivier Heen, Thomas Genet, S. Geller, N. Prigent. An industrial and academical joint experiment on automated verification of a security protocol. In {\em IFIP MWNS'08 Workshop}, 2008.
\nextconference{BallandBGM-AMAST08}  E. Balland, Y. Boichut, Thomas Genet, P.-E. Moreau. Towards an {E}fficient {I}mplementation of {T}ree {A}utomata {C}ompletion. In {\em Algebraic Methodology and Software Technology, 12th International Conference, AMAST 2008}, Lectures Notes in Computer Science, Vol 5140, pp. 67-82, 2008.
\nextconference{AMAST08:CacheraJensenJobinSotin}  David Cachera, Thomas Jensen, Arnaud Jobin, Pascal Sotin. {L}ong-{R}un {C}ost {A}nalysis by {A}pproximation of {L}inear {O}perators over {D}ioids. In {\em Algebraic Methodology and Software Technology, 12th International Conference, AMAST 2008}, Lectures Notes in Computer Science, Vol 5140, pp. 122-138, 2008.
\nextconference{FMOODS08:HubertJensenPichardie}  Laurent Hubert, Thomas Jensen, David Pichardie. {Semantic foundations and inference of non-null annotations}. In {\em Proc.\ of the 10th International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS'08)}, Lecture Notes in Computer Science, Vol 5051, pp. 132-149, 2008.
\nextconference{PASTE08:Hubert}  Laurent Hubert. A Non-Null annotation inferencer for Java bytecode. In {\em Proc.\ of the Workshop on Program Analysis for Software Tools and Engineering (PASTE'08)}, pp. 36-42, 2008.
\nextconference{FICS08:Pichardie}  David Pichardie. {Building certified static analysers by modular construction of well-founded lattices}. In {\em Proc. of the 1st International Conference on Foundations of Informatics, Computing and Software (FICS'08)}, Electronic Notes in Theoretical Computer Science, Vol 212, pp. 225-239, 2008.
\nextconference{SEFM08}  Gilles Barthe, César Kunz, David Pichardie, Juli\'an Samborski Forlese. Preservation of Proof Obligations for Hybrid Certificates. In {\em Proc.\ of the 6th IEEE International Conferences on Software Engineering and Formal Methods (SEFM'08)}, pp. 127-136, 2008.
\nextconference{FMCO7:BCGJP}  Gilles Barthe, Pierre Crégut, Benjamin Grégoire, Thomas Jensen, David Pichardie. {The MOBIUS Proof Carrying Code infrastructure}. In {\em Proc.\ of the 6th International Symposium on Formal Methods for Components and Objects (FMCO'07)}, Lecture Notes in Computer Science, Vol 5382, pp. 1-24, 2008.
\nextconference{GP08}  A. Gotlieb, M. Petit. Constraint reasonning in Path-oriented Random Testing. In {\em 32nd Annual IEEE International Computer Software and Applications Conference (COMPSAC'08)}, {4 pages}, Turku, Finland,  2008.
\nextconference{albert07:_verif_java_bytec_trans_analy}  Elvira Albert, Miguel Gómez-Zamalloa, Laurent Hubert, Germ\'a Puebla. Verification of Java Bytecode Using Analysis and Transformation of Logic Programs. In {\em PADL}, pp. 124-139, 2007.
\nextconference{BoichutGJL-RTA07}  Y. Boichut, T. Genet, T. Jensen, L. Leroux. Rewriting {A}pproximations for {F}ast {P}rototyping of {S}tatic {A}nalyzers. In {\em RTA}, LNCS, Vol 4533, pp. 48-62, 2007.
\nextconference{BoichutGGH-SAR07}  Y. Boichut, T. Genet, Y. Glouche, O. Heen. {U}sing {A}nimation to {I}mprove {F}ormal {S}pecifications of {S}ecurity {P}rotocols. In {\em Joint conference SAR-SSI}, 2007.
\nextconference{BessonJensenTurpin:esop07}  F. Besson, T. Jensen, T. Turpin. Small Witnesses for Abstract Interpretation-Based proofs. In {\em Proc. of 16th European Symposium on Programming (ESOP'07)}, LNCS, Vol 4421, pp. 268-283, 2007.
\nextconference{BPR07}  G. Barthe, D. Pichardie, T. Rezk. {A Certified Lightweight Non-Interference Java Bytecode Verifier}. In {\em Proc.\ of 16th European Symposium on Programming (ESOP'07)}, Lecture Notes in Computer Science, Vol 4421, pp. 125-140, 2007.
\nextconference{PG07b}  M. Petit, A. Gotlieb. Uniform Selection of Feasible Paths as a Stochastic Constraint Problem. In {\em Proceedings of International Conference on Quality Software (QSIC'07)}, IEEE, Portland, USA, October 2007.
\nextconference{PG07a}  M. Petit, A. Gotlieb. Boosting Probabilistic Choice Operators. In {\em Proceedings of Principles and Practices of Constraint Programming}, Springer Verlag, LNCS 4741, pp. 559-573, Providence, USA, September 2007.
\nextconference{DGD07a}  T. Denmat, A. Gotlieb, M. Ducasse. An Abstract Interpretation Based Combinator for Modeling While Loops in Constraint Programming. In {\em Proceedings of Principles and Practices of Constraint Programming (CP'07)}, Springer Verlag, LNCS 4741, pp. 241-255, Providence, USA,  2007.
\nextconference{DGD07b}  T. Denmat, A. Gotlieb, M. Ducasse. Improving Constraint-Based Testing with Dynamic Linear Relaxations. In {\em 18th IEEE International Symposium on Software Reliability Engineering (ISSRE' 2007)}, Trollhättan, Sweden,  2007.
\nextconference{CBG07}  F. Charreteur, B. Botella, A. Gotlieb. Modelling dynamic memory management in Constraint-Based Testing. In {\em TAIC-PART (Testing: Academic and Industrial Conference)}, pp. 111-120, Windsor, UK,  2007.
\nextconference{leguernic07ift}  G. Le Guernic. {I}nformation {F}low {T}esting. In {\em Proceedings of the Annual Asian Computing Science Conference}, Lecture Notes in Computer Science, Vol 4846, pp. 33-47,  2007.
\nextconference{LeGuernic2007acmocp}  G. Le Guernic. {A}utomaton-based {C}onfidentiality {M}onitoring of {C}oncurrent {P}rograms. In {\em Proceedings of the 20th IEEE Computer Security Foundations Symposium (CSFS20)}, pp. 218-232,  2007.
\nextconference{Besson:types06}  F. Besson. Fast Reflexive Arithmetic Tactics: the linear case and beyond. In {\em Types for Proofs and Programs (TYPES'06)}, LNCS, Vol 4502, pp. 48-62, 2006.
\nextconference{BartheFPR06}  Gilles Barthe, Julien Forest, David Pichardie, Vlad Rusu. Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant. In {\em Proc\. of 8th International Symposium on Functional and Logic Programming (FLOPS'06)}, Lecture Notes in Computer Science, Vol 3945, pp. 114-129, 2006.
\nextconference{EAAI:BessonJensenPichardie}  F. Besson, T. Jensen, D. Pichardie. {A PCC Architecture based on Certified Abstract Interpretation}. In {\em Proc. of 1st International Workshop on Emerging Applications of Abstract Interpretation (EAAI'06)}, ENTCS, 2006.
\nextconference{ESORICS-06-BJD}  Frédéric Besson, Guillaume Dufay, Thomas Jensen. A Formal Model of Access Control for Mobile Interactive Devices. In {\em 11th European Symposium On Research In Computer Security (ESORICS'06)}, Lecture Notes in Computer Science, Vol 4189, 2006.
\nextconference{BoichutG-RTA06}  Y. Boichut, T. Genet. {F}easible {T}race {R}econstruction for {R}ewriting {A}pproximations. In {\em RTA}, LNCS, Vol 4098, pp. 123-135, 2006.
\nextconference{Animator}  Y. Glouche, T. Genet, O. Heen, O. Courtay. {A} {S}ecurity {P}rotocol {A}nimator {T}ool for {AVISPA}. In {\em ARTIST-2 workshop on security of embedded systems, Pisa (Italy)}, 2006.
\nextconference{SCJ06}  Pascal Sotin, David Cachera, Thomas Jensen. {Quantitative Static Analysis over semirings: analysing cache behaviour for Java Card}. In {\em 4th International Workshop on Quantitative Aspects of Programming Languages (QAPL 2006)}, Electronic Notes in Theoretical Computer Science, Vol 164, pp. 153-167, 2006.
\nextconference{GBJS06}  Gurvan Le Guernic, Anindya Banerjee, Thomas Jensen, David Schmidt. Automaton-based Confidentiality Monitoring. In {\em 11th Annual Asian Computing Science Conference (ASIAN'06)}, {to appear}, Lecture Notes in Computer Science, Vol 4435, Tokyo, Japan, December 2006.
\nextconference{leguernic06jmbrowser}  N. Bonnel, G. Le Guernic. {S}ystème de recherche de méthodes {J}ava basé sur leur signature. In {\em Proceedings of Majecstic 2006}, November 2006.
\nextconference{GP06}  A. Gotlieb, M. Petit. Path-oriented random testing. In {\em Proceedings of the International Workshop on Random Testing}, pp. 28-35, Portland, USA, July 2006.
\nextconference{PG06}  M. Petit, A. Gotlieb. Raisonner et filtrer avec un choix probabiliste partiellement connu. In {\em Deuxièmes Journées Francophones de Programmation par Contraintes}, N\^imes, France, June 2006.
\nextconference{GG06}  S. Gouraud, A. Gotlieb. Using CHRs to generate test cases for the JCVM. In {\em Eighth International Symposium on Practical Aspects of Declarative Languages, PADL 06}, Lecture Notes in Computer Science, Vol 3819, Charleston, South Carolina, January 2006.
\nextconference{GB06}  A. Gotlieb, P. Bernard. A Semi-empirical Model of Test Quality in Symmetric Testing: Application to Testing Java Card APIs. In {\em Sixth International Conference on Quality Software (QSIC'06)}, Beijing, China,  2006.
\nextconference{BBG06}  B. Blanc, F. Bouquet, A. Gotlieb, B. Jeannet, T. Jéron, B. Legeard, B. Marre, C. Michel, M. Rueher. The V3F project. In {\em Proceedings of Workshop on Constraints in Software Testing, Verification and Analysis (CSTVA'06)}, Nantes, France,  2006.
\nextconference{GBW06}  A. Gotlieb, B. Botella, M. Watel. Inka: Ten years after the first ideas. In {\em 19th International Conference on Software \& Systems Engineering and their Applications (ICSSEA'06)}, Paris, France,  2006.
\nextconference{LeGuernic2006acm}  G. Le Guernic, A. Banerjee, T. Jensen, D. Schmidt. {A}utomata-based {C}onfidentiality {M}onitoring. In {\em Proceedings of the Annual Asian Computing Science Conference}, {To appear}, Lecture Notes in Computer Science, Vol 4435,  2006.
\nextconference{Pich05ParamConcr}  David Pichardie. Modular proof principles for parameterized concretizations. In {\em Proc.\ of 2nd International Workshop on Construction and Analysis of Safe, Secure and Interoperable Smart Devices (CASSIS 2005)}, Lecture Notes in Computer Science, pp. 138-154, 2005.
\nextconference{CaJePiSc05MemoryUsage}  David Cachera, Thomas Jensen, David Pichardie, Gerardo Schneider. {Certified Memory Usage Analysis}. In {\em Proc\. of 13th International Symposium on Formal Methods (FM'05)}, Lecture Notes in Computer Science, 2005.
\nextconference{MorCacCHARME05}  Katell Morin-Allory, David Cachera. {Proving Parameterized Systems: {The} Use of Pseudo-Pipelines in Polyhedral Logic}. In {\em Proc. of 13th CHARME conference}, Lecture Notes in Computer Science, pp. 376-379, 2005.
\nextconference{Sotin05}  David Cachera, Thomas Jensen, Pascal Sotin. Estimating Cache Misses with Semi-Modules and Quantitative Abstraction. In {\em Proc. of IST-APPSEM II Workshop on Applied Semantics}, 2005.
\nextconference{leguernic05flic}  G. Le Guernic, J. Perret. {FL}-system's {I}ntelligent {C}ache. In {\em Proceedings of Majecstic 2005}, Alexandre Vautier, Sylvie Saget (Eds), pp. 79-88, November 2005.
\nextconference{denmat05b}  T. Denmat, M. Ducassé, O. Ridoux. Data mining and cross-checking of execution traces. A 	re-interpretation of {Jones, Harrold and Stasko} test 	information visualization. In {\em Proceedings of the 20th IEEE/ACM International 	Conference on Automated Software Engineering}, {See RR-5661 for a long version 	of this article}, T. Ellman, A. Zisman (Eds), November 2005.
\nextconference{DGD05}  T. Denmat, A. Gotlieb, M. Ducassé. Proving or Disproving Likely Invariants with Constraint 	Reasoning. In {\em Proceedings of the 15th Workshop on Logic-based 	Method for Programming Environments}, {Satelite event of International Conference on Logic 	Programming (ICLP'2005). Published in Computer Research Repository cs.SE/0508108}, A. Serebrenik (Eds), Sitges, SPAIN, October 2005.
\nextconference{GDB05a}  A. Gotlieb, T. Denmat, B. Botella. Goal-oriented test data generation for programs with pointer variables. In {\em 29th IEEE Annual International Computer Software and Applications Conference (COMPSAC'05)}, {6 pages}, pp. 449-454, Edinburh, Scotland, July 2005.
\nextconference{LeGuernic2005mif}  G. Le Guernic, T. Jensen. {M}onitoring {I}nformation {F}low. In {\em Proceedings of the Workshop on Foundations of Computer Security}, Andrei Sabelfeld (Eds), pp. 19-30, June 2005.
\nextconference{GDB05b}  A. Gotlieb, T. Denmat, B. Botella. Constraint-based test data generation in the presence of stack-directed pointers. In {\em 20th IEEE/ACM International Conference on Automated Software Engineering (ASE'05)}, {4 pages, short paper}, Long Beach, CA, USA,  2005.
\nextconference{GG05}  S.D. Gouraud, A. Gotlieb. Utilisation des CHRs pour générer des cas de test fonctionnel pour la Machine Virtuelle Java Card. In {\em Premières Journées Francophones de Programmation par Contraintes (JFPC'05)}, Lens, FRANCE,  2005.
\nextconference{CachJen:esop04}  David Cachera, Thomas Jensen, David Pichardie, Vlad Rusu. Extracting a data flow analyser in constructive logic. In {\em Proc. ESOP'04}, Springer LNCS, pp. 385-400, 2004.
\nextconference{PetitGotlieb:04:poster}  Matthieu Petit, Arnaud Gotlieb. Probabilistic choice operators as global constraints : application to statistical software testing. In {\em Poster presentation in ICLP'04}, Springer LNCS, pp. 471-472, 2004.
\nextconference{PG04}  Matthieu Petit, Arnaud Gotlieb. An ongoing work on statistical structural testing via probabilistic concurrent constraint programming. In {\em Proc. of SIVOES-MODEVA workshop}, St Malo, France, November 2004.
\nextconference{Aertryck:03:UMLCasting}  Lionel van Aertryck, Thomas Jensen. UML-CASTING: Test synthesis from UML models using 		 constraint resolution. In {\em Proc. Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL'2003)}, J-M. Jézéquel (Eds), 2003.
\nextconference{Besson:03:Modular}  F. Besson, T. Jensen. Modular Class Analysis with DATALOG. In {\em Proc. of 10th Static Analysis Symposium (SAS 2003)}, R. Cousot (Eds), pp. 19-36, 2003.
\nextconference{GenetJKP-COCV03}  T. Genet, T. Jensen, V. Kodati, D. Pichardie. A {J}ava {C}ard {C}{A}{P} Converter in {PVS}. In {\em Proceedings of the 2nd International Workshop on Compiler Optimization Meets Compiler Verification (COCV 2003)}, 2003.
\nextconference{GenetTTVTT-wits03}  T. Genet, Y.-M. Tang-Talpin, V. Viet Triem Tong. {V}erification of {C}opy {P}rotection {C}ryptographic {P}rotocol using {A}pproximations of {T}erm {R}ewriting {S}ystems. In {\em In Proceedings of {W}orkshop on {I}ssues in the {T}heory of {S}ecurity}, 2003.
\nextconference{Gotlieb:03:MetaTest}  A. Gotlieb, B. Botella. Automated Metamorphic Testing. In {\em Proc. of the 27th IEEE Annual International Computer Software and Applications Conference (COMPSAC)}, {3th to 7th November}, Dallas, TX, USA, 2003.
\nextconference{Gotlieb:03:SymTest}  Arnaud Gotlieb. Exploiting Symmetries to Test Programs. In {\em Proc. of 14th IEEE International Symposium on Software 		 Reliability Engineering (ISSRE 2003)}, {17th to 20th November}, Denver, Colorado, USA, 2003.
\nextconference{CacPic03}  David Cachera, David Pichardie. {Embedding of Systems of Affine Recurrence Equations in Coq}. In {\em {Proc. TPHOLs 2003, 16th International Conference on Theorem Proving in Higher Order Logics }}, LNCS, Rome, Italy, September 2003.
\nextconference{CacMor03}  David Cachera, Katell Morin-Allory. {Verification of Control Properties in the Polyhedral Model}. In {\em Proc. 1st MEMOCODE conference}, Mont-St-Michel, France, June 2003.
\nextconference{FeuilladeG-FTP03}  G. Feuillade, T. Genet. Reachability in conditional term rewriting systems. In {\em FTP'2003, International Workshop on First-Order Theorem Proving}, Electronic Notes in Theoretical Computer Science, Vol 86 n. 1, June 2003.
\nextconference{Besson:02:CallingContexts}  F. Besson, Thomas de Grenier de Latour, T. Jensen. Secure calling contexts for stack inspection. In {\em Proc. of 4th Int Conf. on Principles and Practice of Declarative Programming (PPDP 2002)}, pp. 76-87, 2002.
\nextconference{Eluard:02:SecureObjectFlow}  Marc Éluard, Thomas Jensen. Secure object flow analysis for Java Card. In {\em Proc. of 5th Smart Card Research and Advanced Application Conference (Cardis'02)}, 2002.
\nextconference{Jensen:02:Iteration}  Thomas Jensen, Florimond Ployette, Olivier Ridoux. Iteration schemes for fixed point conputation. In {\em Proc. of 4th Int workshop on Fixed Points in Computer Science (FICS'02)}, A. Ingolfsdottir, Z. Esik (Eds), pp. 69-76, 2002.
\nextconference{BePi01Convexhull}  David Pichardie, Yves Bertot. {Formalizing Convex Hulls Algorithms}. In {\em Proc.\ of 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'01)}, Lecture Notes in Computer Science, pp. 346-361, 2001.
\nextconference{GenetVTTong-LPAR01}  T. Genet, Valérie Viet Triem Tong. {R}eachability {A}nalysis of {T}erm {R}ewriting {S}ystems with {Timbuk}. In {\em 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning}, Lectures Notes in Artificial Intelligence, Vol 2250, pp. 691-702, 2001.
\nextconference{Jensen:01:ClassAnalysis}  T. Jensen, F. Spoto. Class analysis of object-oriented programs through abstract interpretation. In {\em Proc. of Foundations of Software Science and Computation Structures (FoSSaCS'01)}, F. Honsell, M. Miculan (Eds), pp. 261-275, 2001.
\nextconference{Siveroni:01:Nordsec}  Igor Siveroni, Thomas Jensen, Marc Éluard. A Formal Specification of the Java Card Applet Firewall. In {\em Nordic Workshop on Secure IT-Systems}, Hanne Riis Nielson (Eds), November 2001.
\nextconference{Eluard:01:Esmart}  Marc Éluard, Thomas Jensen, Ewen Denney. An Operational Semantics of the Java Card Firewall. In {\em Smart Card Programming and Security (e-Smart 2001}, Isabelle Attali, Thomas Jensen (Eds), Vol Springer LNCS vol. 2140, September 2001.
\nextconference{Denney:00:Correctness}  E. Denney, T. Jensen. Correctness of {J}ava {C}ard method lookup via logical relations. In {\em Proc. of European Symp. on Programming (ESOP 2000)}, Lecture Notes in Computer Science, pp. 104-118, 2000.
\nextconference{GenetKlay-CADE00}  T. Genet, F. Klay. {R}ewriting for {C}ryptographic {P}rotocol {V}erification. In {\em Proceedings 17th International Conference on Automated 		 Deduction}, Lecture Notes in Artificial Intelligence, Vol 1831, 2000.
\nextconference{SAS99:BJT}  F. Besson, T. Jensen, J.P. Talpin. {P}olyhedral {A}nalysis for {S}ynchronous {L}anguages. In {\em International Static Analysis Symposium, SAS'99}, Gilberto Filé (Eds), Lecture Notes in Computer Science, Vol 1694, September 1999.
\nextconference{SSP99}  T. Jensen, D. Le Métayer, T. Thorn. Verification of control flow based security properties. In {\em Proc.\ of the 20th IEEE Symp. on Security and Privacy}, pp. 89-103, May 1999.
\nextconference{Jensen:98:Inference}  T. Jensen. Inference of polymorphic and conditional strictness properties. In {\em Proc. of 25th {ACM} Symposium on Principles of Programming Languages}, pp. 209-221, 1998.
\nextconference{tjdlmtt-iccl98}  T. Jensen, D. Le Métayer, T. Thorn. Security and Dynamic Class Loading in Java: A Formalisation. In {\em Proceedings of the 1998 IEEE International Conference on Computer Languages}, pp. 4-15, May 1998.
\end{bibliconference}
\paragraph{National Conferences}
\begin{bibliconferencenat}
\nextconferencenat{SSTIC10:JAVASEC}  Guillaume Hiet, Frédéric Guihéry, Goulven Guiheux, David Pichardie, Christian Brunette. Sécurité de la plate-forme d'exécution {J}ava : limites et propositions d'améliorations. In {\em Proc.\ of Symposium sur la sécurité des technologies de l'information et des communications (SSTIC 2010)}, 2010.
\nextconferencenat{MidtgaardJ08}  J. Midtgaard, Thomas Jensen. A Calculational Approach to Control-Flow Analysis by Abstract Interpretation. In {\em Proc. of the 15th Static Aanalysi Symposium}, LNCS, Vol 5079, pp. 347-362, 2008.
\nextconferencenat{SARSSI08}  Olivier Heen, Gilles Guette, Thomas Genet. Anonymity within trust communities. In {\em SAR-SSI 2008, 3rd conference on security in network architectures and information systems}, Nora Cuppens-Boulahia, Philippe Owezarski (Eds), pp. 183-195, 2008.
\nextconferencenat{CG08}  F. Charreteur, A. Gotlieb. Raisonnement à contraintes pour le test de bytecode Java. In {\em quatrièmes Journées Francophones de Programmation par Contraintes (JFPC'08)}, pp. 11-20, Nantes, France, June 2008.
\end{bibliconferencenat}
\paragraph{Research Reports}
\begin{biblirr}
\nextrr{boichut:2010:inria-00501487:1}  Yohan Boichut, Benoît Boyer, Thomas Genet, Axel Legay. Fast Equational Abstraction Refinement for Regular Tree Model Checking. Rapport de recherche INRIA, July 2010.
\nextrr{Turpin09}  Tiphaine Turpin, Frédéric Besson, Thomas Jensen. Computing the Least Fix-point Semantics of Logic Programs Using BDDs. Rapport de recherche INRIA, No 7107, 2009.
\nextrr{DEMANGE:2009:INRIA-00414099:2}  Delphine Demange, Thomas Jensen, David Pichardie. {A} {P}rovably {C}orrect {S}tackless {I}ntermediate {R}epresentation {F}or {J}ava {B}ytecode. Rapport de recherche INRIA, No 0, 2009.
\nextrr{BJPT:polycert:techreport}  F. Besson, T. Jensen, D. Pichardie, T. Turpin. Result certification for relational program analysis. Rapport de recherche Inria, No 6333, September 2007.
\nextrr{CacJenSotRR07}  David Cachera, Thomas Jensen, Pascal Sotin. Long-Run Cost Analysis by Approximation of Linear Operators over Dioids. Rapport de recherche INRIA, No 6338,  2007.
\nextrr{LeGuernic2006abnim}  G. Le Guernic, A. Banerjee, D. Schmidt. {A}utomaton-based {N}on-interference {M}onitoring. Rapport de recherche {D}epartment of {C}omputing and {I}nformation {S}ciences, {C}ollege of {E}ngineering, {K}ansas {S}tate {U}niversity, No 2006, April 2006.
\nextrr{CacMorRR05}  David Cachera, Katell Morin-Allory. Proving Parameterized Systems: the use of a widening operator and pseudo-pipelines in polyhedral logic. Rapport de recherche TIMA-IMAG, No 0, 2005.
\nextrr{RR-5751}  F. Besson, T. Jensen, D. Pichardie. A PCC Architecture based on Certified Abstract Interpretation. Rapport de recherche INRIA, No 0, November 2005.
\nextrr{denmat05c}  T. Denmat, M. Ducassé, O. Ridoux. Data Mining and Cross-checking of Execution Traces. {A} re-interpretation of {Jones}, {Harrold} and {Stasko} test information visualization ({Long} version). Rapport de recherche INRIA, No 0, August 2005.
\nextrr{CacMorRR03}  David Cachera, Katell Morin-Allory. {Verification of Control Properties in the Polyhedral Model}. Rapport de recherche INRIA, No 1515, 2003.
\nextrr{CacPicRR03}  David Cachera, David Pichardie. {Proof Tactics for the Verification of Structured Systems of Affine Recurrence Equations}. Rapport de recherche INRIA, No 1511, 2003.
\nextrr{FeuilladeGVTT-RR03}  G. Feuillade, T. Genet, V. Viet Triem Tong. {R}eachability {A}nalysis over {T}erm {R}ewriting {S}ystems. Rapport de recherche INRIA, No 0, 2003.
\nextrr{GenetVTTong-RR02}  T. Genet, V. Viet Triem Tong. {P}roving {N}egative {C}onjectures on {E}quational {T}heories using {I}nduction and {A}bstract {I}nterpretation. Rapport de recherche INRIA, No 0, 2002.
\nextrr{GenetVTTong-RR01}  Thomas Genet, Valérie Viet Triem Tong. {R}eachability {A}nalysis of {T}erm {R}ewriting {S}ystems with {Timbuk} (extended version). Rapport de recherche INRIA, No 0, 2001.
\nextrr{GenetK-CNET99}  T. Genet, F. Klay. {R}ewriting for {C}ryptographic {P}rotocol {V}erification (extended version). Rapport de recherche INRIA, No 3921, 2000.
\nextrr{jensen:98:verification}  T. Jensen, D. Le Métayer, T. Thorn. Verification of control flow based security policies. Rapport de recherche IRISA, No 1210, 1998.
\end{biblirr}
\paragraph{Misc}
\begin{biblimisc}
\nextmisc{FOSAD09:BessonCacheraJensenPichardie}  Fré Besson, David Cachera, Thomas Jensen, David Pichardie. Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures, pp. 223-257, 2009.
\nextmisc{HeenGH-MISC08}  Olivier Heen, Thomas Genet, E. Houssay. Votre protocole est-il vérifié?, pp. 58-68, September 2008.
\nextmisc{Genet-Interstices08}  Thomas Genet. Le protocole cryptographique de paiement par carte bancaire, February 2008.
\nextmisc{PichardieTI08}  David Pichardie. Les codes porteurs de preuve, pp. 8-9,  2008.
\nextmisc{span-manual}  Y. Glouche, T. Genet. {S}{P}{A}{N} - A {S}ecurity {P}rotocol {A}{N}imator for {AVISPA} - {U}ser {M}anual, 2006.
\nextmisc{LeGuernic2003ras_misc}  G. Le Guernic. {R}oles \& {S}ecurity, {\em 03411 Abstracts Collection - Language-Based Security}, No 3411, Dagstuhl, Germany, October 2005.
\nextmisc{Timbuk-manual}  T. Genet. {T}imbuk 2.0 - A {T}ree {A}utomata {L}ibrary - {R}eference {M}anual and {T}utorial, IRISA / Université de Rennes 1, 2003.
\nextmisc{brevet99}  E. Denney, P. Fradet, C. Goire, T. Jensen, D. Le Métayer. Procédé de vérification de transformateurs de codes pour un système embarqué, notamment sur une carte à puce, July 1999.
\end{biblimisc}
\paragraph{Thesis}
\begin{biblithese}
\nextthese{HdrCachera}  David Cachera. {\em Analyses statiques : certifier et quantifier}. Habilitation à diriger les recherches de l'École normale supérieure de Cachan, 2010.
\nextthese{PhdHubert}  Laurent Hubert. {\em Foundations and Implementation of a Tool Bench for Static Analysis of Java Bytecode Programsr}. Thèse de l'Université de Rennes 1, December 2010.
\nextthese{Boyer10}  Benoît Boyer. {\em Réécriture d'automates certifiée pour la vérification de modèle}. Thèse de l'Université Européenne de Bretagne, December 2010.
\nextthese{charreteur:2010:tel-00497785:1}  Florence Charreteur. {\em Modélisation par contraintes de programmes en bytecode Java pour la génération automatique de tests}. Thèse de l'Université Européenne de Bretagne, March 2010.
\nextthese{HdrGenet}  Thomas Genet. {\em Reachability Analysis of Rewriting for Software Verification}. Habilitation à diriger les recherches de l'Université de Rennes 1, 2009.
\nextthese{SotinPhD}  Pascal Sotin. {\em Quantitative Aspects of Program Analysis}. Thèse de l'Université Rennes 1, December 2008.
\nextthese{TurpinPhD}  T. Turpin. {\em Pruning program invariants, Élagage d'invariants de programmes}. Thèse de l'Université Rennes 1, December 2008.
\nextthese{PetitPhD}  M. Petit. {\em Test statistique structurel par résolution de contraintes de choix probabiliste}. Thèse de l'Université Rennes 1, July 2008.
\nextthese{DenmatPhD}  T. Denmat. {\em Contraintes et abstractions pour la génération automatique de données de test}. Thèse de l'Université Rennes 1, June 2008.
\nextthese{Guernic:phd:07}  G. Le Guernic. {\em Confidentiality Enforcement Using Dynamic Information Flow Analyses}. Thèse de l'Université Rennes 1 and Kansas State University, September 2007.
\nextthese{hongtuanha:phd:07}  S. Hong Tuan Ha. {\em Programmation par aspects et tissage de propriétés - Application à l'ordonnancement et à la disponibilité}. Thèse de l'Université Rennes 1, January 2007.
\nextthese{PicThe05}  David Pichardie. {\em Interprétation abstraite en logique intuitionniste : extraction d'analyseurs Java certiés}. Thèse de l'Université Rennes 1, Rennes, France, December 2005.
\nextthese{alloy-morin04}  Katell Morin-Allory. {\em Vérification formelle dans le modèle polyédrique}. Thèse de l'Université de Rennes 1, October 2004.
\nextthese{Morin04}  B. Morin. {\em Corrélation d'alertes issues d'outils de détection 	d'intrusions avec prise en compte d'informations sur le 	système surveillé}. Thèse de l'INSA de Rennes, February 2004.
\nextthese{VietTriemTong-PhD03}  V. Viet Triem Tong. {\em Automates d'arbres et réécriture pour l'étude de problèmes d'accessibilité}. Thèse de l'Université Rennes 1, 2003.
\nextthese{Besson:02:PhD}  F. Besson. {\em Analyse modulaire de programmes}. Thèse de l'Université de Rennes 1, 2002.
\nextthese{Rouvrais02a}  Siegfried Rouvrais. {\em Utilisation d'agents mobiles pour la construction de services distribués}. Thèse de l'Université de Rennes 1, July 2002.
\nextthese{Eluard:01:PhD}  Marc Éluard. {\em Analyse de sécurité pour la certification d'applications Java Card}. Thèse de l'Université de Rennes 1, December 2001.
\nextthese{HDR-PF}  Pascal Fradet. {\em Approches langages pour la conception et la mise en oeuvre de programmes}. Habilitation à diriger les recherches de l'Université de Rennes 1, November 2000.
\nextthese{ThesePerin}  Michaël Périn. {\em {Spécifications graphiques multi-vues : formalisation et vérification de cohérence}}. Thèse de l'IFSIC, October 2000.
\nextthese{Jensen:99:Hab}  Thomas Jensen. {\em Analyse statiques de programmes : fondements et applications}. Habilitation à diriger les recherches de l'Université de Rennes 1, December 1999.
\nextthese{TT99}  T. Thorn. {\em Vérification de politiques de sécurité par analyse de programmes}. Thèse de l'Université de Rennes I, Ifsic, Irisa, February 1999.
\nextthese{Mallet98c}  J. Mallet. {\em Compilation d'un langage spécialisé pour machine massivement parallèle}. Thèse de l'Université de Rennes I, Ifsic, Irisa, 1998.
\nextthese{Nicolas-these98}  V.-A. Nicolas. {\em Preuves de propriétés de classes de programmes par dérivation systématique de jeux de test}. Thèse de l'Université de Rennes I, Ifsic, Irisa, December 1998.
\nextthese{Gouranton:97:DerivationD}  V. Gouranton. {\em Dérivation d'analyseurs dynamiques et statiques à partir de spécifications opérationnelles}. Thèse de l'Université de Rennes I, Ifsic, Irisa, 1997.
\end{biblithese}