Publications 2011

International Conferences

  1. 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.
  2. 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.
  3. 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
  4. 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
  5. 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.
  6. 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.
  7. 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.

Research Reports

  1. Gilles Barthe, Delphine Demange, David Pichardie. A formally verified SSA-based middle-end compiler. Research Report INRIA, October 2011. download
  2. Nadjib Lazaar, Nourredine Aribi, Arnaud Gotlieb, Yahia Lebbah. Negation for Free!. Research Report INRIA, No 0, October 2011. download
  3. David Cachera, Thomas Jensen, Arnaud Jobin, Florent Kirchner. Fast inference of polynomial invariants for imperative programs. Research Report INRIA, No 0, May 2011. download

Thesis

  1. Mickael Delahaye. Généralisation de chemins infaisables pour l'exécution symbolique dynamique. PhD Thesis University of Rennes 1, 2011.
  2. Arnaud Gotlieb. Contributions to Constraint-Based Testing. Habilitation à diriger des recherches University of Rennes 1, 2011.
  3. 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.