All the publications

Load the BibTeX file

Books

  1. Sandrine Blazy, Christine Paulin-Mohring, David Pichardie. Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings. Sandrine Blazy, Christine Paulin-Mohring, David PichardieS. Blazy, C. Paulin-Mohring, D. Pichardie (eds.), Lecture Notes in Computer Science, Springer, 2013. download

Proceedings

  1. M. Huisman, T. Jensen (eds.). J. Logic and Algebraic Programming. Special issue on Formal Methods for Smart Cards, vol. 58(1-2). Elsevier, 2004.
  2. Isabelle Attali, Thomas Jensen (eds.). Smart Card Programming and Security (e-Smart 2001). Springer LNCS vol. 2140, September 2001.
  3. I. Attali, T. Jensen (eds.). Proceedings of the International Workshop on Java Card (Java Card 2000). Inria, Cannes, France, September 2000.

Academic Journals

  1. David Cachera, Thomas Jensen, Arnaud Jobin, Florent Kirchner. Inference of polynomial invariants for imperative programs: a farewell to Gröbner bases. Science of Computer Programming, To appear, 2014. download
  2. Gilles Barthe, David Pichardie, Tamara Rezk. A certified lightweight non-interference Java bytecode verifier. Mathematical Structures in Computer Science, 23(5):1032-1081, June 2013. download
  3. Jan Midtgaard, Thomas Jensen. Control-Flow Analysis by Abstract Interpretation. Information and Computation, 2012.
  4. Jan Midtgaard, Thomas Jensen. Control Flow Analysis of Function Calls and Returns by Abstract Interpretation. Information and Computation, 211:49-76, 2012.
  5. Thomas Jensen, Florent Kirchner, David Pichardie. Secure the Clones: Static Enforcement of Policies for Secure Object Copying. Logical Methods in Computer Science (LMCS), 8(2), 2012.
  6. David Cachera, Thomas Jensen, Arnaud Jobin, Pascal Sotin. Long-Run Cost Analysis by Approximation of Linear Operators over Dioids. Mathematical Structures in Computer Science, 20(4):589-624, 2010.
  7. Frédéric Besson, Thomas Jensen, Guillaume Dufay, David Pichardie. Verifying Resource Access Control on Mobile Interactive Devices. Journal of Computer Security, 18(6):971-998, 2010.
  8. Thomas Genet, Vlad Rusu. Equational Approximations for Tree Automata Completion. Journal of Symbolic Computation, 45(5):574-597, May 2010(5):574-597, 2010.
  9. A. Gotlieb. TCAS software verification using Constraint Programming. The Knowledge Engineering Review, Under revision, 2009.
  10. Sandrine Blazy, Xavier Leroy. Mechanized semantics for the Clight subset of the C language. Journal of Automated Reasoning, 43(3):263-288, 2009.
  11. A. Gotlieb, T. Denmat, B. Botella. Goal-oriented test data generation for pointer programs. Information and Software Technology, 49(9):1030-1044, 2007.
  12. Frédéric Besson, Thomas Jensen, David Pichardie. Proof-Carrying Code from Certified Abstract Interpretation to Fixpoint Compression. Theoretical Computer Science, 364(3):273-291, 2006.
  13. B. Botella, A. Gotlieb, C. Michel. Symbolic execution of floating-point computations. The Software Testing, Verification and Reliability journal, to appear, 2006.
  14. F. Besson, T. de Grenier de Latour, T. Jensen. Interfaces for stack inspection. Journal of Functional Programming, 15(2):179-217, 2005. download
  15. David Cachera, Thomas Jensen, David Pichardie, Vlad Rusu. Extracting a Data Flow Analyser in Constructive Logic. Theoretical Computer Science, 2005.
  16. David Cachera, Katell Morin-Allory. Verification of safety properties for parameterized regular systems. Trans. on Embedded Computing Systems, 4(2):228-266, 2005.
  17. M. Eluard, T. Jensen. Vérification du contrôle d'accès dans des cartes à puce multi-application. Technique et Science Informatiques, 23(3):323-358, 2004.
  18. G. Feuillade, T. Genet, V. Viet Triem Tong. Reachability Analysis over Term Rewriting Systems. Journal of Automated Reasoning, 33 (3-4):341-383, 2004. download
  19. T. Jensen, J.-L. Lanet. Modélisation et vérification dans les cartes à puce. Revue d'électricité et de l'électronique, 6/7:89-94, 2004.
  20. A. Banerjee, T. Jensen. Control-flow analysis with rank-2 intersection types. Mathematical Structures in Computer Science, 13(1):87-124, 2003.
  21. F. Spoto, T. Jensen. Class Analyses as Abstract Interpretations of Trace Semantics. ACM Transactions on Programming Languages and Systems (TOPLAS), 25(5):578-630, 2003.
  22. E. Denney, T. Jensen. Correctness of Java Card method lookup via logical relations. Theoretical Computer Science, 283:305-331, 2002.
  23. F. Besson, T. Jensen, D. Le Métayer, T. Thorn. Model ckecking security properties of control flow graphs. Journal of Computer Security, 9:217-250, 2001. download
  24. T. Jensen. Disjunctive Program Analysis for Algebraic Data Types. ACM Transactions on Programming Languages and Systems, 19(5):752-804, 1997. ps

Book Chapters

  1. Xavier Leroy, W, Andrew Appel, Sandrine Blazy, Gordon Stewart. The CompCert memory model. In Program Logics for Certified Compilers, Andrew W. Appel (ed.), Cambridge University Press, December 2013. download
  2. Benjamin Blanc, Arnaud Gotlieb, Claude Michel. Constraints in Software Testing, Verification and Analysis. In Trends in Constraint Programming, Fré Benhamou, Narendra Jussien, Barry O'Sullivan (eds.), Chap. 7, pp. 333-368, ISTE, London, UK, May 2007.
  3. T. Jensen. Types in program analysis. In 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.

International Conferences

  1. Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Catalin Hritcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, Andrew Tolmach. A Verified Information-Flow Architecture. In 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), To appear, San Diego, CA, United States, 2014. download
  2. R. Bagnara, M. Carlier, R. Gori, A. Gotlieb. Symbolic Path-Oriented Test Data Generation for Floating-Point Programs. In Proc. of the 6th IEEE Int. Conf. on Software Testing, Verification and Validation (ICST'13), Luxembourg, Luxembourg, 2013. download
  3. Sandrine Blazy, Vincent Laporte, André Maroneze, David Pichardie. Formal Verification of a C Value Analysis Based on Abstract Interpretation. In SAS - 20th Static Analysis Symposium, Manuel Fahndrich, Francesco Logozzo (eds.), Volume Lecture Notes in Computer Science, Pages 324-344, Seattle, United States, 2013. download
  4. Sandrine Blazy, André Maroneze, David Pichardie. Formal Verification of Loop Bound Estimation for WCET Analysis. In VSTTE - Verified Software: Theories, Tools and Experiments, Ernie Cohen, Andrey Rybalchenko (eds.), Lecture Notes in Computer Science, Volume 8164, Pages 281-303, Menlo Park, United States, 2013. download
  5. Frédéric Besson, Nataliia Bielova, Thomas Jensen. Hybrid Information Flow Monitoring Against Web Tracking. In CSF - 2013 IEEE 26th Computer Security Foundations Symposium, New Orleans, United States, 2013. download
  6. Frédéric Besson, Pierre-Emmanuel Cornilleau, Thomas Jensen. Result Certification of Static Program Analysers with Automated Theorem Provers. In VSTTE 2013 - Fifth Working Conference on Verified Software: Theories, Tools and Experiments, Atherthon, United States, 2013. download
  7. Delphine Demange, Vincent Laporte, Lei Zhao, David Pichardie, Suresh Jagannathan, Jan Vitek. Plan B: A Buffered Memory Model for Java. In Proc. of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, Rome, Italy, 2013. download
  8. Thomas Genet, Tristan Le Gall, Axel Legay, Valérie Murat. Tree Regular Model Checking for Lattice-Based Automata. In CIAA - 18th International Conference on Implementation and Application of Automata, LNCS, Volume 7982, Halifax, Canada, 2013. download
  9. Martin Bodin, Arthur Charguéraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, Daiva Naudziuniene, Alan Schmitt, Gareth Smith. A Trusted Mechanised JavaScript Specification. In POPL 2014 - 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, United States, November 2013. download
  10. Jael Kriener, Andy King, Sandrine Blazy. Proofs You Can Believe In. Proving Equivalences Between Prolog Semantics in Coq. In 15th International Symposium on Principles and Practice of Declarative Programming (PPDP), Tom Schrijvers (ed.), Pages 37-48, Madrid, Spain, September 2013. download
  11. Ivan Lanese, Michael Lienhardt, Antares, Claudio Mezzina, Alan Schmitt, Jean-Bernard Stefani. Concurrent Flexible Reversibility. In 22nd European Symposium on Programming, ESOP 2013, Matthias Felleisen, Philippa Gardner (eds.), Lecture Notes in Computer Science (LNCS), Volume 7792, Pages 370-390, Rome, Italy, March 2013. download
  12. Martin Bodin, Alan Schmitt. A Certified JavaScript Interpreter. In JFLA - Journées francophones des langages applicatifs, Damien Pous, Christine Tasson (eds.), Aussois, France, February 2013. download
  13. Ricardo Bedin Franca, Sandrine Blazy, Denis Favre-Felix, Xavier Leroy, Marc Pantel, Jean Souyris. Formally verified optimizing compilation in ACG-based flight control software. In ERTS2 congress, to appear, 2012.
  14. Pierre-Alain Fouque, Nicolas Guillermin, Delphine Leresteux, Mehdi Tibouchi, Jean-Christophe Zapalowicz. Attacking RSA-CRT Signatures with Faults on Montgomery Multiplication. In Cryptographic Hardware and Embedded Systems - CHES 2012, Lecture Notes in Computer Science, Volume 7428, Pages 447-462, 2012. download
  15. Marion Daubignard, Pierre-Alain Fouque, Yassine Lakhnech. Generic Indifferentiability Proofs of Hash Designs. In 25th IEEE Computer Security Foundations Symposium, CSF 2012, Pages 340-353, 2012. download
  16. Michel Abdalla, Pierre-Alain Fouque, Vadim Lyubashevsky, Mehdi Tibouchi. Tightly-Secure Signatures from Lossy Identification Schemes. In Advances in Cryptology - EUROCRYPT 2012, Lecture Notes in Computer Science, Volume 7237, Pages 572-590, 2012. download
  17. Jiqiang Lu, Yongzhuang Wei, Enes Pasalic, Pierre-Alain Fouque. Meet-in-the-Middle Attack on Reduced Versions of the Camellia Block Cipher. In International Workshop on Security, IWSEC 2012, Lecture Notes in Computer Science, Volume 7631, Pages 197-215, 2012. download
  18. Pierre-Alain Fouque, Mehdi Tibouchi. Indifferentiable Hashing to Barreto-Naehrig Curves. In LATINCRYPT 2012, Lecture Notes in Computer Science, Volume 7533, Pages 1-17, 2012. download
  19. Pierre-Alain Fouque, Delphine Leresteux, Fré Valette. Using faults for buffer overflow effects. In ACM Symposium on Applied Computing, SAC 2012, Pages 1638-1639, 2012. download
  20. Patrick Derbez, Pierre-Alain Fouque, Jé Jean. Faster Chosen-Key Distinguishers on Reduced-Round AES. In Indocrypt 2012, Lecture Notes in Computer Science, Volume 7668, Pages 225-243, 2012. download
  21. Gilles Barthe, Delphine Demange, David Pichardie. A formally verified SSA-based middle-end - Static Single Assignment meets CompCert. In Proc. of 21th European Symposium on Programming (ESOP 2012), Lecture Notes in Computer Science, Volume 7211, Pages 47-66, 2012.
  22. Yohan Boichut, Benoit Boyer, Thomas Genet, Axel Legay. Equational Abstraction Refinement for Certified Tree Regular Model Checking. In ICFEM'12, LNCS, Pages 299-315, Kyoto, Japon, 2012. pdf
  23. T. Genet, Y. Salmon. Proving Reachability Properties on Term Rewriting Systems with Strategies. In 2nd Joint International Workshop on Strategies in Rewriting, Proving and Programming, IWS'12, London, 2012.
  24. Pierre-Emmanuel Cornilleau. Prototyping Static Analysis Certification using Why3. In Boogie 2012: Second International Workshop on Intermediate Verification Languages, 2012.
  25. Frédéric Besson, Pierre-Emmanuel Cornilleau, Ronan Saillard. Walking through the Forest: a Fast EUF Proof-Checking Algorithm. In Second International Workshop on Proof eXchange for Theorem Proving - PxTP 2012, 2012.
  26. David Cachera, Thomas Jensen, Arnaud Jobin, Florent Kirchner. Inference of polynomial invariants for imperative programs: a farewell to Gröbner bases. In SAS - 19th International Static Analysis Symposium - 2012, Projet Région Bretagne CertLogs, Deauville, France, September 2012. download
  27. Ricardo Bedin França, Sandrine Blazy, Denis Favre-Felix, Xavier Leroy, Marc Pantel, Jean Souyris. Formally verified optimizing compilation in ACG-based flight control software. In ERTS2 2012: Embedded Real Time Software and Systems, Toulouse, France, February 2012. download
  28. Frédéric Besson, Pascal Fontaine, Laurent Théry. A Flexible Proof Format for SMT: a Proposal. In Workshop on Proof eXchange for Theorem Proving (PxTP), 2011.
  29. Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie. A Nelson-Oppen based Proof System using Theory Specific Proof Systems. In Workshop on Proof eXchange for Theorem Proving (PxTP), 2011.
  30. Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie. Modular SMT Proofs for Fast Reflexive Checking inside Coq. In First International Conference on Certified Programs and Proofs, Lecture Notes in Computer Science, Volume 7086, Pages 151-166, Kenting, Taiwan, Province De Chine, 2011. download
  31. Yohan Boichut, Thi-Bich-Hanh Dao, Valérie Murat. Characterizing Conclusive Approximations by Logical Formulae. In Reachability Problems 2011, Giorgio Delzanno, Igor Potapov (eds.), Volume LNCS 6945, Gênes, Italy, 2011. download
  32. Thomas Jensen, Florent Kirchner, David Pichardie. Secure the Clones: Static Enforcement of Policies for Secure Object Copying. In Proc. of 20th European Symposium on Programming (ESOP 2011), Lecture Notes in Computer Science, Volume 6602, Pages 317-337, 2011.
  33. M. Carlier, A. Gotlieb. Filtering by ULP Maximum. In Proc. of the IEEE Int. Conf. on Tools for Artificial Intelligence (ICTAI'11), Short paper, 4 pages, 2011.
  34. N. Lazaar, A. Gotlieb, Y. Lebbah. A framework for the automatic correction of Constraint Programs. In 4th IEEE International Conference on Software Testing, Validation and Verification (ICST'11), Berlin, Germany, 2011.
  35. David Cachera, Arnaud Jobin. Injecting Abstract Interpretations into Linear Cost Models. In 8th Workshop on Quantitative Aspects of Programming Languages (QAPL), EPTCS, Paphos, 2010.
  36. Delphine Demange, Thomas Jensen, David Pichardie. A Provably Correct Stackless Intermediate Representation for Java Bytecode. In 8th Asian Symposium on Programming Languages and Systems (APLAS), Lecture Notes in Computer Science, Volume 6461, 2010.
  37. David Cachera, David Pichardie. A Certified Denotational Abstract Interpreter. In Proc.\ of International Conference on Interactive Theorem Proving (ITP-10), Lecture Notes in Computer Science, Volume 6172, Pages 9-24, 2010.
  38. Frédéric Besson, Thomas Jensen, David Pichardie, Tiphaine Turpin. Certified Result Checking for Polyhedral Analysis of Bytecode Programs. In Proc.\ of the 5th International Symposium on Trustworthy Global Computing (TGC 2010), Lecture Notes in Computer Science, Volume 6084, Pages 253-267, 2010.
  39. 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 1st International Conference on Formal Verification of Object-Oriented Software (FoVeOOS), Lecture Notes in Computer Science, 2010.
  40. Laurent Hubert, Thomas Jensen, Vincent Monfort, David Pichardie. Enforcing Secure Object Initialization in Java. In 15th European Symposium on Research in Computer Security (ESORICS), Lecture Notes in Computer Science, Volume 6345, Pages 101-115, 2010.
  41. Helene Kirchner, Kirchner Florent, Claude Kirchner. Constraint Based Strategies. In 18th International Workshop on Functional and Constraint Logic Programming - WFLP 2009, Volume 5979, Pages 13-26, Brésil Brasilia, 2010.
  42. Frédéric Besson. On using an inexact floating-point LP solver for deciding linear arithmetic in an SMT solver. In 8th International Workshop on Satisfiability Modulo Theories, 2010.
  43. A. Gotlieb, M. Leconte, B. Marre. Constraint Solving on Modular Integers. In Proc. of the 9th Int. Workshop on Constraint Modelling and Reformulation (ModRef'10), co-located with CP'2010, St Andrews, Scotland, 2010.
  44. N. Lazaar, A. Gotlieb, Y. Lebbah. Fault Localization in Constraint Programs. In 22th Int. Conf. on Tools with Artificial Intelligence (ICTAI'2010), Arras, France, 2010.
  45. F. Charreteur, A. Gotlieb. Constraint-Based Test Input Generation for Java Bytecode. In Proc. of the 21st IEEE Int. Symp. on Softw. Reliability Engineering (ISSRE'10), San Jose, CA, USA, 2010.
  46. N. Lazaar, A. Gotlieb, Y. Lebbah. On Testing Constraint Programs. In 16th Int. Conf. on Principles and Practices of Constraint Programming (CP'2010), St Andrews, Scotland, 2010.
  47. M. Carlier, C. Dubois, A. Gotlieb. Constraint Reasonning in FOCALTEST. In 5rd International Conference on Software and Data Technologies (ICSOFT'10), Athens, Greece, 2010.
  48. M. Delahaye, B. Botella, A. Gotlieb. Explanation-based generalization of infeasible path. In 3rd IEEE International Conference on Software Testing, Validation and Verification (ICST'10), Paris, France, 2010.
  49. Sandrine Blazy, Benoît Robillard, Andrew W. Appel. Formal Verification of Coalescing Graph-Coloring Register Allocation. In 19th European Symposium on Programming (ESOP), Volume 6012, Pages 145-164, Chypre Paphos, March 2010.
  50. Delphine Demange, David Sands. All Secrets Great and Small. In Proceedings of the 18th European Symposium on Programming Languages and Systems: Held As Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, ESOP '09, Pages 207-221, Berlin, Heidelberg, 2009.
  51. N. Lazaar, A. Gotlieb, Y. Lebbah. Towards Constraint-Based Local Search for Automatic Test Data Generation. In 1th International Workshop on Search-based Test Data Generation, co-located with ICST 2009, Lillehammer, Norway, 2009.
  52. A. Gotlieb. EUCLIDE: A Constraint-Based Testing platform for critical C programs. In 2th International Conference on Software Testing, Validation and Verification (ICST'09), Denver, CO, 2009.
  53. Gilles Guette, Olivier Heen. A TPM-based Architecture for Improved Security and Anonymity in Vehicular Ad hoc Networks. In In International Vehicular Networking Conference (IEEE VNC 2009), 2009.
  54. Olivier Heen, Gilles Guette, Thomas Genet. On the Unobservability of a Trust Relation in Mobile Ad Hoc Networks. In WISTP 2009 3rd edition, LNCS, Volume 5746, 2009.
  55. A. Gotlieb, M. Petit. Towards a Theory for Testing Non-terminating Programs. In 33nd Annual IEEE International Computer Software and Applications Conference (COMPSAC'09), 6 pages, Seattle, USA, 2009.
  56. Jan Midtgaard, Thomas Jensen. Control-flow analysis of function calls and returns by abstract interpretation. In Proceedings of the 14th ACM international conference on Functional programming, Pages 287-298, 2009.
  57. Frédéric Besson. CPA beats oo-CFA. In Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs, Pages 1-6, 2009.
  58. Sandrine Blazy, Benoît Robillard. Live-range Unsplitting for Faster Optimal Coalescing. In Proceedings of the ACM SIGPLAN/SIGBED 2009 conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2009), Pages 70-79, 2009. download
  59. B. Boyer, T. Genet. Verifying Temporal Regular properties of Abstractions of Term Rewriting Systems. In Proc. of RULE'09, EPTCS, Volume 21, 2009.
  60. Frédéric Dabrowski, David Pichardie. A Certified Data Race Analysis for a Java-like Language. In Proc.\ of 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs'09), Lecture Notes in Computer Science, Volume 5674, Pages 212-227, 2009.
  61. David Cachera, David Pichardie. Comparing Techniques for Certified Static Analysis. In Proc.\ of the 1st NASA Formal Methods Symposium (NFM'09), Pages 111-115, 2009.
  62. Laurent Hubert, David Pichardie. Soundly Handling Static Fields: Issues, Semantics and Analysis. In Proc.\ of the 4th International Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE'09), Electronic Notes in Theoretical Computer Science, Volume 253, Pages 15-30, 2009.
  63. Frédéric Besson, Thomas Jensen, T. Turpin. Computing stack maps with interfaces. In Proc. of the 22nd European Conference on Object-Oriented Programming (ECOOP 2008), LNCS, Volume 5142, Pages 642-666, 2008.
  64. J. Midtgaard, Thomas Jensen. A Calculational Approach to Control-Flow Analysis by Abstract Interpretation. In Static Analysis, 15th International Symposium, SAS 2008, Lectures Notes in Computer Science, Volume 5079, Pages 347-362, 2008.
  65. B. Boyer, Thomas Genet, Thomas Jensen. Certifying a Tree Automata Completion Checker. In 4th International Joint Conference, IJCAR 2008, Lectures Notes in Computer Science, Volume 5195, Pages 347-362, 2008.
  66. Olivier Heen, Thomas Genet, S. Geller, N. Prigent. An industrial and academical joint experiment on automated verification of a security protocol. In IFIP MWNS'08 Workshop, 2008.
  67. E. Balland, Y. Boichut, Thomas Genet, P.-E. Moreau. Towards an Efficient Implementation of Tree Automata Completion. In Algebraic Methodology and Software Technology, 12th International Conference, AMAST 2008, Lectures Notes in Computer Science, Volume 5140, Pages 67-82, 2008.
  68. David Cachera, Thomas Jensen, Arnaud Jobin, Pascal Sotin. Long-Run Cost Analysis by Approximation of Linear Operators over Dioids. In Algebraic Methodology and Software Technology, 12th International Conference, AMAST 2008, Lectures Notes in Computer Science, Volume 5140, Pages 122-138, 2008.
  69. Laurent Hubert, Thomas Jensen, David Pichardie. Semantic foundations and inference of non-null annotations. In Proc.\ of the 10th International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS'08), Lecture Notes in Computer Science, Volume 5051, Pages 132-149, 2008.
  70. Laurent Hubert. A Non-Null annotation inferencer for Java bytecode. In Proc.\ of the Workshop on Program Analysis for Software Tools and Engineering (PASTE'08), Pages 36-42, 2008.
  71. David Pichardie. Building certified static analysers by modular construction of well-founded lattices. In Proc. of the 1st International Conference on Foundations of Informatics, Computing and Software (FICS'08), Electronic Notes in Theoretical Computer Science, Volume 212, Pages 225-239, 2008.
  72. Gilles Barthe, César Kunz, David Pichardie, Juli\'an Samborski Forlese. Preservation of Proof Obligations for Hybrid Certificates. In Proc.\ of the 6th IEEE International Conferences on Software Engineering and Formal Methods (SEFM'08), Pages 127-136, 2008.
  73. Gilles Barthe, Pierre Crégut, Benjamin Grégoire, Thomas Jensen, David Pichardie. The MOBIUS Proof Carrying Code infrastructure. In Proc.\ of the 6th International Symposium on Formal Methods for Components and Objects (FMCO'07), Lecture Notes in Computer Science, Volume 5382, Pages 1-24, 2008.
  74. A. Gotlieb, M. Petit. Constraint reasonning in Path-oriented Random Testing. In 32nd Annual IEEE International Computer Software and Applications Conference (COMPSAC'08), 4 pages, Turku, Finland, 2008.
  75. T. Denmat, A. Gotlieb, M. Ducasse. An Abstract Interpretation Based Combinator for Modeling While Loops in Constraint Programming. In Proceedings of Principles and Practices of Constraint Programming (CP'07), Springer Verlag, LNCS 4741, Pages 241-255, Providence, USA, 2007.
  76. T. Denmat, A. Gotlieb, M. Ducasse. Improving Constraint-Based Testing with Dynamic Linear Relaxations. In 18th IEEE International Symposium on Software Reliability Engineering (ISSRE' 2007), Trollhättan, Sweden, 2007.
  77. F. Charreteur, B. Botella, A. Gotlieb. Modelling dynamic memory management in Constraint-Based Testing. In TAIC-PART (Testing: Academic and Industrial Conference), Pages 111-120, Windsor, UK, 2007.
  78. Elvira Albert, Miguel Gómez-Zamalloa, Laurent Hubert, Germ\'a Puebla. Verification of Java Bytecode Using Analysis and Transformation of Logic Programs. In PADL, Pages 124-139, 2007. pdf
  79. Y. Boichut, T. Genet, T. Jensen, L. Leroux. Rewriting Approximations for Fast Prototyping of Static Analyzers. In RTA, LNCS, Volume 4533, Pages 48-62, 2007.
  80. Y. Boichut, T. Genet, Y. Glouche, O. Heen. Using Animation to Improve Formal Specifications of Security Protocols. In Joint conference SAR-SSI, 2007.
  81. F. Besson, T. Jensen, T. Turpin. Small Witnesses for Abstract Interpretation-Based proofs. In Proc. of 16th European Symposium on Programming (ESOP'07), LNCS, Volume 4421, Pages 268-283, 2007.
  82. G. Barthe, D. Pichardie, T. Rezk. A Certified Lightweight Non-Interference Java Bytecode Verifier. In Proc.\ of 16th European Symposium on Programming (ESOP'07), Lecture Notes in Computer Science, Volume 4421, Pages 125-140, 2007.
  83. G. Le Guernic. Information Flow Testing. In Proceedings of the Annual Asian Computing Science Conference, Lecture Notes in Computer Science, Volume 4846, Pages 33-47, 2007.
  84. G. Le Guernic. Automaton-based Confidentiality Monitoring of Concurrent Programs. In Proceedings of the 20th IEEE Computer Security Foundations Symposium (CSFS20), Pages 218-232, 2007.
  85. M. Petit, A. Gotlieb. Uniform Selection of Feasible Paths as a Stochastic Constraint Problem. In Proceedings of International Conference on Quality Software (QSIC'07), IEEE, Portland, USA, October 2007.
  86. M. Petit, A. Gotlieb. Boosting Probabilistic Choice Operators. In Proceedings of Principles and Practices of Constraint Programming, Springer Verlag, LNCS 4741, Pages 559-573, Providence, USA, September 2007.
  87. A. Gotlieb, P. Bernard. A Semi-empirical Model of Test Quality in Symmetric Testing: Application to Testing Java Card APIs. In Sixth International Conference on Quality Software (QSIC'06), Beijing, China, 2006.
  88. B. Blanc, F. Bouquet, A. Gotlieb, B. Jeannet, T. Jéron, B. Legeard, B. Marre, C. Michel, M. Rueher. The V3F project. In Proceedings of Workshop on Constraints in Software Testing, Verification and Analysis (CSTVA'06), Nantes, France, 2006.
  89. F. Besson. Fast Reflexive Arithmetic Tactics: the linear case and beyond. In Types for Proofs and Programs (TYPES'06), LNCS, Volume 4502, Pages 48-62, 2006. pdf
  90. Gilles Barthe, Julien Forest, David Pichardie, Vlad Rusu. Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant. In Proc\. of 8th International Symposium on Functional and Logic Programming (FLOPS'06), Lecture Notes in Computer Science, Volume 3945, Pages 114-129, 2006.
  91. F. Besson, T. Jensen, D. Pichardie. A PCC Architecture based on Certified Abstract Interpretation. In Proc. of 1st International Workshop on Emerging Applications of Abstract Interpretation (EAAI'06), ENTCS, 2006. download
  92. Frédéric Besson, Guillaume Dufay, Thomas Jensen. A Formal Model of Access Control for Mobile Interactive Devices. In 11th European Symposium On Research In Computer Security (ESORICS'06), Lecture Notes in Computer Science, Volume 4189, 2006. download
  93. Y. Boichut, T. Genet. Feasible Trace Reconstruction for Rewriting Approximations. In RTA, LNCS, Volume 4098, Pages 123-135, 2006.
  94. Y. Glouche, T. Genet, O. Heen, O. Courtay. A Security Protocol Animator Tool for AVISPA. In ARTIST-2 workshop on security of embedded systems, Pisa (Italy), 2006. download
  95. Pascal Sotin, David Cachera, Thomas Jensen. Quantitative Static Analysis over semirings: analysing cache behaviour for Java Card. In 4th International Workshop on Quantitative Aspects of Programming Languages (QAPL 2006), Electronic Notes in Theoretical Computer Science, Volume 164, Pages 153-167, 2006.
  96. A. Gotlieb, B. Botella, M. Watel. Inka: Ten years after the first ideas. In 19th International Conference on Software & Systems Engineering and their Applications (ICSSEA'06), Paris, France, 2006.
  97. G. Le Guernic, A. Banerjee, T. Jensen, D. Schmidt. Automata-based Confidentiality Monitoring. In Proceedings of the Annual Asian Computing Science Conference, Lecture Notes in Computer Science, To appear, Volume 4435, 2006. pdf
  98. Gurvan Le Guernic, Anindya Banerjee, Thomas Jensen, David Schmidt. Automaton-based Confidentiality Monitoring. In 11th Annual Asian Computing Science Conference (ASIAN'06), Lecture Notes in Computer Science, to appear, Volume 4435, Tokyo, Japan, December 2006.
  99. N. Bonnel, G. Le Guernic. Système de recherche de méthodes Java basé sur leur signature. In Proceedings of Majecstic 2006, November 2006. pdf
  100. A. Gotlieb, M. Petit. Path-oriented random testing. In Proceedings of the International Workshop on Random Testing, Pages 28-35, Portland, USA, July 2006.
  101. M. Petit, A. Gotlieb. Raisonner et filtrer avec un choix probabiliste partiellement connu. In Deuxièmes Journées Francophones de Programmation par Contraintes, N\^imes, France, June 2006.
  102. S. Gouraud, A. Gotlieb. Using CHRs to generate test cases for the JCVM. In Eighth International Symposium on Practical Aspects of Declarative Languages, PADL 06, Lecture Notes in Computer Science, Volume 3819, Charleston, South Carolina, January 2006.
  103. David Pichardie. Modular proof principles for parameterized concretizations. In Proc.\ of 2nd International Workshop on Construction and Analysis of Safe, Secure and Interoperable Smart Devices (CASSIS 2005), Lecture Notes in Computer Science, Pages 138-154, 2005.
  104. David Cachera, Thomas Jensen, David Pichardie, Gerardo Schneider. Certified Memory Usage Analysis. In Proc\. of 13th International Symposium on Formal Methods (FM'05), Lecture Notes in Computer Science, 2005.
  105. A. Gotlieb, T. Denmat, B. Botella. Constraint-based test data generation in the presence of stack-directed pointers. In 20th IEEE/ACM International Conference on Automated Software Engineering (ASE'05), 4 pages, short paper, Long Beach, CA, USA, 2005.
  106. S.D. Gouraud, A. Gotlieb. Utilisation des CHRs pour générer des cas de test fonctionnel pour la Machine Virtuelle Java Card. In Premières Journées Francophones de Programmation par Contraintes (JFPC'05), Lens, FRANCE, 2005.
  107. Katell Morin-Allory, David Cachera. Proving Parameterized Systems: The Use of Pseudo-Pipelines in Polyhedral Logic. In Proc. of 13th CHARME conference, Lecture Notes in Computer Science, Pages 376-379, 2005.
  108. David Cachera, Thomas Jensen, Pascal Sotin. Estimating Cache Misses with Semi-Modules and Quantitative Abstraction. In Proc. of IST-APPSEM II Workshop on Applied Semantics, 2005.
  109. G. Le Guernic, J. Perret. FL-system's Intelligent Cache. In Proceedings of Majecstic 2005, Alexandre Vautier, Sylvie Saget (eds.), Pages 79-88, November 2005. pdf
  110. 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 Proceedings of the 20th IEEE/ACM International Conference on Automated Software Engineering, T. Ellman, A. Zisman (eds.), See RR-5661 for a long version of this article, November 2005.
  111. T. Denmat, A. Gotlieb, M. Ducassé. Proving or Disproving Likely Invariants with Constraint Reasoning. In Proceedings of the 15th Workshop on Logic-based Method for Programming Environments, A. Serebrenik (ed.), Satelite event of International Conference on Logic Programming (ICLP'2005). Published in Computer Research Repository cs.SE/0508108, Sitges, SPAIN, October 2005. download
  112. A. Gotlieb, T. Denmat, B. Botella. Goal-oriented test data generation for programs with pointer variables. In 29th IEEE Annual International Computer Software and Applications Conference (COMPSAC'05), 6 pages, Pages 449-454, Edinburh, Scotland, July 2005.
  113. G. Le Guernic, T. Jensen. Monitoring Information Flow. In Proceedings of the Workshop on Foundations of Computer Security, Andrei Sabelfeld (ed.), Pages 19-30, June 2005. pdf
  114. David Cachera, Thomas Jensen, David Pichardie, Vlad Rusu. Extracting a data flow analyser in constructive logic. In Proc. ESOP'04, Springer LNCS, Pages 385-400, 2004.
  115. Matthieu Petit, Arnaud Gotlieb. Probabilistic choice operators as global constraints : application to statistical software testing. In Poster presentation in ICLP'04, Springer LNCS, Pages 471-472, 2004.
  116. Matthieu Petit, Arnaud Gotlieb. An ongoing work on statistical structural testing via probabilistic concurrent constraint programming. In Proc. of SIVOES-MODEVA workshop, St Malo, France, November 2004.
  117. Lionel van Aertryck, Thomas Jensen. UML-CASTING: Test synthesis from UML models using constraint resolution. In Proc. Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL'2003), J-M. Jézéquel (ed.), 2003.
  118. F. Besson, T. Jensen. Modular Class Analysis with DATALOG. In Proc. of 10th Static Analysis Symposium (SAS 2003), R. Cousot (ed.), Pages 19-36, 2003. download
  119. T. Genet, T. Jensen, V. Kodati, D. Pichardie. A Java Card CAP Converter in PVS. In Proceedings of the 2nd International Workshop on Compiler Optimization Meets Compiler Verification (COCV 2003), 2003. download
  120. T. Genet, Y.-M. Tang-Talpin, V. Viet Triem Tong. Verification of Copy Protection Cryptographic Protocol using Approximations of Term Rewriting Systems. In In Proceedings of Workshop on Issues in the Theory of Security, 2003. download
  121. A. Gotlieb, B. Botella. Automated Metamorphic Testing. In Proc. of the 27th IEEE Annual International Computer Software and Applications Conference (COMPSAC), 3th to 7th November, Dallas, TX, USA, 2003.
  122. Arnaud Gotlieb. Exploiting Symmetries to Test Programs. In Proc. of 14th IEEE International Symposium on Software Reliability Engineering (ISSRE 2003), 17th to 20th November, Denver, Colorado, USA, 2003.
  123. David Cachera, David Pichardie. Embedding of Systems of Affine Recurrence Equations in Coq. In Proc. TPHOLs 2003, 16th International Conference on Theorem Proving in Higher Order Logics , LNCS, Rome, Italy, September 2003. ps
  124. David Cachera, Katell Morin-Allory. Verification of Control Properties in the Polyhedral Model. In Proc. 1st MEMOCODE conference, Mont-St-Michel, France, June 2003. ps
  125. G. Feuillade, T. Genet. Reachability in conditional term rewriting systems. In FTP'2003, International Workshop on First-Order Theorem Proving, Electronic Notes in Theoretical Computer Science, Volume 86 n. 1, June 2003. download
  126. F. Besson, Thomas de Grenier de Latour, T. Jensen. Secure calling contexts for stack inspection. In Proc. of 4th Int Conf. on Principles and Practice of Declarative Programming (PPDP 2002), Pages 76-87, 2002. download
  127. Marc Éluard, Thomas Jensen. Secure object flow analysis for Java Card. In Proc. of 5th Smart Card Research and Advanced Application Conference (Cardis'02), 2002.
  128. Thomas Jensen, Florimond Ployette, Olivier Ridoux. Iteration schemes for fixed point conputation. In Proc. of 4th Int workshop on Fixed Points in Computer Science (FICS'02), A. Ingolfsdottir, Z. Esik (eds.), Pages 69-76, 2002.
  129. David Pichardie, Yves Bertot. Formalizing Convex Hulls Algorithms. In Proc.\ of 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'01), Lecture Notes in Computer Science, Pages 346-361, 2001.
  130. T. Genet, Valérie Viet Triem Tong. Reachability Analysis of Term Rewriting Systems with Timbuk. In 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, Lectures Notes in Artificial Intelligence, Volume 2250, Pages 691-702, 2001. ps
  131. T. Jensen, F. Spoto. Class analysis of object-oriented programs through abstract interpretation. In Proc. of Foundations of Software Science and Computation Structures (FoSSaCS'01), F. Honsell, M. Miculan (eds.), Pages 261-275, 2001.
  132. Igor Siveroni, Thomas Jensen, Marc Éluard. A Formal Specification of the Java Card Applet Firewall. In Nordic Workshop on Secure IT-Systems, Hanne Riis Nielson (ed.), November 2001.
  133. Marc Éluard, Thomas Jensen, Ewen Denney. An Operational Semantics of the Java Card Firewall. In Smart Card Programming and Security (e-Smart 2001, Isabelle Attali, Thomas Jensen (eds.), Volume Springer LNCS vol. 2140, September 2001.
  134. E. Denney, T. Jensen. Correctness of Java Card method lookup via logical relations. In Proc. of European Symp. on Programming (ESOP 2000), Lecture Notes in Computer Science, Pages 104-118, 2000.
  135. T. Genet, F. Klay. Rewriting for Cryptographic Protocol Verification. In Proceedings 17th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, Volume 1831, 2000. ps
  136. F. Besson, T. Jensen, J.P. Talpin. Polyhedral Analysis for Synchronous Languages. In International Static Analysis Symposium, SAS'99, Gilberto Filé (ed.), Lecture Notes in Computer Science, Volume 1694, September 1999.
  137. T. Jensen, D. Le Métayer, T. Thorn. Verification of control flow based security properties. In Proc.\ of the 20th IEEE Symp. on Security and Privacy, Pages 89-103, May 1999.
  138. T. Jensen. Inference of polymorphic and conditional strictness properties. In Proc. of 25th ACM Symposium on Principles of Programming Languages, Pages 209-221, 1998. ps
  139. T. Jensen, D. Le Métayer, T. Thorn. Security and Dynamic Class Loading in Java: A Formalisation. In Proceedings of the 1998 IEEE International Conference on Computer Languages, Pages 4-15, May 1998. ps

National Conferences

  1. Simon Boulier, Alan Schmitt. Formalisation de HOCore en Coq. In JFLA - Journées Francophones des Langages Applicatifs - 2012, Carnac, France, February 2012. download
  2. Guillaume Hiet, Frédéric Guihéry, Goulven Guiheux, David Pichardie, Christian Brunette. Sécurité de la plate-forme d'exécution Java : limites et propositions d'améliorations. In Proc.\ of Symposium sur la sécurité des technologies de l'information et des communications (SSTIC 2010), 2010.
  3. J. Midtgaard, Thomas Jensen. A Calculational Approach to Control-Flow Analysis by Abstract Interpretation. In Proc. of the 15th Static Aanalysi Symposium, LNCS, Volume 5079, Pages 347-362, 2008.
  4. Olivier Heen, Gilles Guette, Thomas Genet. Anonymity within trust communities. In SAR-SSI 2008, 3rd conference on security in network architectures and information systems, Nora Cuppens-Boulahia, Philippe Owezarski (eds.), Pages 183-195, 2008.
  5. F. Charreteur, A. Gotlieb. Raisonnement à contraintes pour le test de bytecode Java. In quatrièmes Journées Francophones de Programmation par Contraintes (JFPC'08), Pages 11-20, Nantes, France, June 2008.

Research Reports

  1. Thomas Genet. Towards Static Analysis of Functional Programs using Tree Automata Completion. December 2013. download
  2. Thomas Genet, Yann Salmon. Reachability Analysis of Innermost Rewriting. July 2013. download
  3. Thomas Genet, Yann Salmon. Tree Automata Completion for Static Analysis of Functional Programs. January 2013. download
  4. Pierre Genevès, Nabil Layaïda, Alan Schmitt. Logical Combinators for Rich Type Systems. Research Report INRIA, No 0, July 2012. download
  5. Xavier Leroy, W, Andrew Appel, Sandrine Blazy, Gordon Stewart. The CompCert Memory Model, Version 2. Research Report INRIA, No 0, June 2012. download
  6. Thomas Genet, Tristan Le Gall, Axel Legay, Valérie Murat. Tree Regular Model Checking for Lattice-Based Automata. Technical Report INRIA, No 0, April 2012. download
  7. Nadjib Lazaar, Nourredine Aribi, Arnaud Gotlieb, Yahia Lebbah. Negation for Free!. Research Report INRIA, No 0, October 2011. download
  8. Gilles Barthe, Delphine Demange, David Pichardie. A formally verified SSA-based middle-end compiler. Research Report INRIA, October 2011. download
  9. David Cachera, Thomas Jensen, Arnaud Jobin, Florent Kirchner. Fast inference of polynomial invariants for imperative programs. Research Report INRIA, No 0, May 2011. download
  10. Yohan Boichut, Benoît Boyer, Thomas Genet, Axel Legay. Fast Equational Abstraction Refinement for Regular Tree Model Checking. Rapport Technique INRIA, July 2010.
  11. Tiphaine Turpin, Frédéric Besson, Thomas Jensen. Computing the Least Fix-point Semantics of Logic Programs Using BDDs. Research Report INRIA, No 7107, 2009.
  12. Delphine Demange, Thomas Jensen, David Pichardie. A Provably Correct Stackless Intermediate Representation For Java Bytecode. Research Report INRIA, No 0, 2009. download
  13. David Cachera, Thomas Jensen, Pascal Sotin. Long-Run Cost Analysis by Approximation of Linear Operators over Dioids. Research Report INRIA, No 6338, 2007. download
  14. F. Besson, T. Jensen, D. Pichardie, T. Turpin. Result certification for relational program analysis. Research Report Inria, No 6333, September 2007. download
  15. G. Le Guernic, A. Banerjee, D. Schmidt. Automaton-based Non-interference Monitoring. Research Report Department of Computing and Information Sciences, College of Engineering, Kansas State University, No 2006, April 2006. download
  16. David Cachera, Katell Morin-Allory. Proving Parameterized Systems: the use of a widening operator and pseudo-pipelines in polyhedral logic. Research Report TIMA-IMAG, No 0, 2005.
  17. F. Besson, T. Jensen, D. Pichardie. A PCC Architecture based on Certified Abstract Interpretation. Research Report INRIA, No 0, November 2005.
  18. 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). Research Report INRIA, No 0, August 2005.
  19. David Cachera, Katell Morin-Allory. Verification of Control Properties in the Polyhedral Model. Research Report INRIA, No 1515, 2003. ps
  20. David Cachera, David Pichardie. Proof Tactics for the Verification of Structured Systems of Affine Recurrence Equations. Research Report INRIA, No 1511, 2003. ps
  21. G. Feuillade, T. Genet, V. Viet Triem Tong. Reachability Analysis over Term Rewriting Systems. Research Report INRIA, No 0, 2003. ps
  22. T. Genet, V. Viet Triem Tong. Proving Negative Conjectures on Equational Theories using Induction and Abstract Interpretation. Research Report INRIA, No 0, 2002. ps
  23. Thomas Genet, Valérie Viet Triem Tong. Reachability Analysis of Term Rewriting Systems with Timbuk (extended version). Technical Report INRIA, No 0, 2001. ps
  24. T. Genet, F. Klay. Rewriting for Cryptographic Protocol Verification (extended version). Technical Report INRIA, No 3921, 2000. ps
  25. T. Jensen, D. Le Métayer, T. Thorn. Verification of control flow based security policies. Research Report IRISA, No 1210, 1998. ps

Misc

  1. 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.
  2. David Pichardie. Les codes porteurs de preuve. pp. 8-9, 2008.
  3. Olivier Heen, Thomas Genet, E. Houssay. Votre protocole est-il vérifié?. pp. 58-68, September 2008.
  4. Thomas Genet. Le protocole cryptographique de paiement par carte bancaire. February 2008. download
  5. Y. Glouche, T. Genet. SPAN - A Security Protocol ANimator for AVISPA - User Manual. 2006. download
  6. G. Le Guernic. Roles & Security. 03411 Abstracts Collection - Language-Based Security, No 3411, Dagstuhl, Germany, October 2005. download
  7. T. Genet. Timbuk 2.0 - A Tree Automata Library - Reference Manual and Tutorial. IRISA / Université de Rennes 1, 2003. download
  8. 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.

Thesis

  1. Zhoulai Fu. Static analysis of numerical properties in the presence of pointers. PhD Thesis Université Rennes 1 and Université européenne de Bretagne, July 2013. download
  2. David Pichardie. Toward a Verified Software Toolchain for Java. Habilitation à diriger des recherches ENS Cachan, 2012.
  3. Delphine Demange. Semantic foundations of intermediate program representations. PhD Thesis ENS Cachan, 2012.
  4. Arnaud Jobin. Dioïdes et idéaux de polynômes en analyse statique. PhD Thesis ENS Cachan, 2012.
  5. Arnaud Gotlieb. Contributions to Constraint-Based Testing. Habilitation à diriger des recherches University of Rennes 1, 2011.
  6. Nadjib Lazaar. Méthodologie et outil de test, de localisation de fautes et de correction automatique des programmes contraintes. PhD Thesis University of Rennes 1, 2011.
  7. Mickael Delahaye. Généralisation de chemins infaisables pour l'exécution symbolique dynamique. PhD Thesis University of Rennes 1, 2011.
  8. David Cachera. Analyses statiques : certifier et quantifier. Habilitation à diriger des recherches École normale supérieure de Cachan, 2010.
  9. Laurent Hubert. Foundations and Implementation of a Tool Bench for Static Analysis of Java Bytecode Programs. PhD Thesis Université de Rennes 1, December 2010.
  10. Benoît Boyer. Réécriture d'automates certifiée pour la vérification de modèle. PhD Thesis Université Européenne de Bretagne, December 2010.
  11. Florence Charreteur. Modélisation par contraintes de programmes en bytecode Java pour la génération automatique de tests. PhD Thesis Université Européenne de Bretagne, March 2010.
  12. Thomas Genet. Reachability Analysis of Rewriting for Software Verification. Habilitation à diriger des recherches Université de Rennes 1, 2009.
  13. Pascal Sotin. Quantitative Aspects of Program Analysis. PhD Thesis Université Rennes 1, December 2008.
  14. T. Turpin. Pruning program invariants, Élagage d'invariants de programmes. PhD Thesis Université Rennes 1, December 2008.
  15. M. Petit. Test statistique structurel par résolution de contraintes de choix probabiliste. PhD Thesis Université Rennes 1, July 2008.
  16. T. Denmat. Contraintes et abstractions pour la génération automatique de données de test. PhD Thesis Université Rennes 1, June 2008.
  17. G. Le Guernic. Confidentiality Enforcement Using Dynamic Information Flow Analyses. PhD Thesis Université Rennes 1 and Kansas State University, September 2007.
  18. S. Hong Tuan Ha. Programmation par aspects et tissage de propriétés - Application à l'ordonnancement et à la disponibilité. PhD Thesis Université Rennes 1, January 2007.
  19. David Pichardie. Interprétation abstraite en logique intuitionniste : extraction d'analyseurs Java certiés. PhD Thesis Université Rennes 1, Rennes, France, December 2005.
  20. Katell Morin-Allory. Vérification formelle dans le modèle polyédrique. PhD Thesis Université de Rennes 1, October 2004.
  21. B. Morin. Corrélation d'alertes issues d'outils de détection d'intrusions avec prise en compte d'informations sur le système surveillé. PhD Thesis INSA de Rennes, February 2004.
  22. V. Viet Triem Tong. Automates d'arbres et réécriture pour l'étude de problèmes d'accessibilité. PhD Thesis Université Rennes 1, 2003.
  23. F. Besson. Analyse modulaire de programmes. PhD Thesis Université de Rennes 1, 2002. download
  24. Siegfried Rouvrais. Utilisation d'agents mobiles pour la construction de services distribués. PhD Thesis Université de Rennes 1, July 2002.
  25. Marc Éluard. Analyse de sécurité pour la certification d'applications Java Card. PhD Thesis Université de Rennes 1, December 2001.
  26. Pascal Fradet. Approches langages pour la conception et la mise en oeuvre de programmes. Habilitation à diriger des recherches Université de Rennes 1, November 2000.
  27. Michaël Périn. Spécifications graphiques multi-vues : formalisation et vérification de cohérence. PhD Thesis IFSIC, October 2000.
  28. Thomas Jensen. Analyse statiques de programmes : fondements et applications. Habilitation à diriger des recherches Université de Rennes 1, December 1999.
  29. T. Thorn. Vérification de politiques de sécurité par analyse de programmes. PhD Thesis Université de Rennes I, Ifsic, Irisa, February 1999.
  30. J. Mallet. Compilation d'un langage spécialisé pour machine massivement parallèle. PhD Thesis Université de Rennes I, Ifsic, Irisa, 1998. ps
  31. V.-A. Nicolas. Preuves de propriétés de classes de programmes par dérivation systématique de jeux de test. PhD Thesis Université de Rennes I, Ifsic, Irisa, December 1998. ps
  32. V. Gouranton. Dérivation d'analyseurs dynamiques et statiques à partir de spécifications opérationnelles. PhD Thesis Université de Rennes I, Ifsic, Irisa, 1997. ps

Master's theses

  1. Antoine Bride. Vérification probabiliste de résultats d'analyse statique. June 2012. download