Publications 2013


  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

Academic Journals

  1. 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

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

International Conferences

  1. 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
  2. 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
  3. 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
  4. 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
  5. 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
  6. 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
  7. 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
  8. 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
  9. 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
  10. 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
  11. 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

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


  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