Publications 2012

Academic Journals

  1. 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.
  2. Jan Midtgaard, Thomas Jensen. Control-Flow Analysis by Abstract Interpretation. Information and Computation, 2012.
  3. Jan Midtgaard, Thomas Jensen. Control Flow Analysis of Function Calls and Returns by Abstract Interpretation. Information and Computation, 211:49-76, 2012.

International Conferences

  1. 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
  2. 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.
  3. 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.
  4. 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.
  5. 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
  6. Pierre-Emmanuel Cornilleau. Prototyping Static Analysis Certification using Why3. In Boogie 2012: Second International Workshop on Intermediate Verification Languages, 2012.
  7. 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
  8. 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
  9. 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
  10. 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
  11. 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
  12. 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.
  13. 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
  14. 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
  15. 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

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

Research Reports

  1. Pierre Genevès, Nabil Layaïda, Alan Schmitt. Logical Combinators for Rich Type Systems. Research Report INRIA, No 0, July 2012. download
  2. Xavier Leroy, W, Andrew Appel, Sandrine Blazy, Gordon Stewart. The CompCert Memory Model, Version 2. Research Report INRIA, No 0, June 2012. download
  3. 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

Thesis

  1. Delphine Demange. Semantic foundations of intermediate program representations. PhD Thesis ENS Cachan, 2012.
  2. Arnaud Jobin. Dioïdes et idéaux de polynômes en analyse statique. PhD Thesis ENS Cachan, 2012.
  3. David Pichardie. Toward a Verified Software Toolchain for Java. Habilitation à diriger des recherches ENS Cachan, 2012.

Master's theses

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