EN FR
EN FR


previous Previous | up Home


Bibliography

Major publications by the team in recent years
  • 1G. Barthe, B. Grégoire, S. Heraud, S. Z. Béguelin.

    Computer-Aided Security Proofs for the Working Cryptographer, in: Advances in Cryptology - CRYPTO 2011 - 31st Annual Cryptology Conference, Santa Barbara, CA, USA, August 14-18, 2011. Proceedings, Lecture Notes in Computer Science, Springer, 2011, vol. 6841, pp. 71-90, Best Paper Award.
  • 2Y. Bertot, G. Gonthier, S. O. Biha, I. Paşca.

    Canonical Big Operators, in: Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2008), Lecture Notes in Computer Science, Springer, August 2008, vol. 5170, pp. 12–16.

    http://hal.inria.fr/inria-00331193/
  • 3G. Gonthier, A. Asperti, J. Avigad, Y. Bertot, C. Cohen, F. Garillot, S. Le Roux, A. Mahboubi, R. O'Connor, S. Ould Biha, I. Pasca, L. Rideau, A. Solovyev, E. Tassi, L. Théry.

    A Machine-Checked Proof of the Odd Order Theorem, in: ITP 2013, 4th Conference on Interactive Theorem Proving, Rennes, France, S. Blazy, C. Paulin, D. Pichardie (editors), LNCS, Springer, 2013, vol. 7998, pp. 163-179. [ DOI : 10.1007/978-3-642-39634-2_14 ]

    http://hal.inria.fr/hal-00816699
  • 4G. Gonthier, A. Mahboubi, L. Rideau, E. Tassi, L. Théry.

    A Modular Formalisation of Finite Group Theory, in: Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2007), K. Schneider, J. Brandt (editors), LNCS, Springer-Verlag, September 2007, vol. 4732, pp. 86-101.

    http://hal.inria.fr/inria-00139131
Publications of the year

Articles in International Peer-Reviewed Journals

International Conferences with Proceedings

  • 7R. Affeldt, C. Cohen.

    Formal Foundations of 3D Geometry to Model Robot Manipulators, in: Conference on Certified Programs and Proofs 2017, Paris, France, January 2017.

    https://hal.inria.fr/hal-01414753
  • 8J. B. Almeida, M. Barbosa, G. Barthe, A. Blot, B. Grégoire, V. Laporte, T. Oliveira, H. Pacheco, B. Schmidt, P.-Y. Strub.

    Jasmin: High-Assurance and High-Speed Cryptography, in: CCS 2017 - Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, Dallas, United States, October 2017, pp. 1-17.

    https://hal.archives-ouvertes.fr/hal-01649140
  • 9J. B. Almeida, M. Barbosa, G. Barthe, F. Dupressoir, B. Grégoire, V. Laporte, V. Pereira.

    A Fast and Verified Software Stack for Secure Function Evaluation, in: CCS 2017 - ACM SIGSAC Conference on Computer and Communications Security, Dallas, United States, Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30 - November 03, 2017, ACM, October 2017, pp. 1-18.

    https://hal.archives-ouvertes.fr/hal-01649104
  • 10G. Barthe, F. Dupressoir, S. Faust, B. Grégoire, F.-X. Standaert, P.-Y. Strub.

    Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model, in: Advances in Cryptology - EUROCRYPT 2017 - 36th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Paris, France, Advances in Cryptology - EUROCRYPT 2017 - 36th Annual International Conference on the Theory and Applications of Cryptographic Techniques, April 2017, vol. 10210, pp. 535–566.

    https://hal.inria.fr/hal-01414009
  • 11G. Barthe, T. Espitau, B. Grégoire, J. Hsu, P.-Y. Strub.

    Proving uniformity and independence by self-composition and coupling, in: LPAR 2017 - International Conferences on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, LPAR 2017 - International Conferences on Logic for Programming, Artificial Intelligence and Reasoning, May 2017, 19 p.

    http://hal.upmc.fr/hal-01541198
  • 12G. Barthe, B. Grégoire, J. Hsu, P.-Y. Strub.

    Coupling proofs are probabilistic product programs, in: POPL 2017 - Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, Paris, France, ACM, January 2017, vol. 52, no 1, pp. 161-174. [ DOI : 10.1145/3009837.3009896 ]

    https://hal.archives-ouvertes.fr/hal-01649028
  • 13S. Bernard.

    Formalization of the Lindemann-Weierstrass Theorem, in: Interactive Theorem Proving, Brasilia, Brazil, September 2017.

    https://hal.inria.fr/hal-01647563
  • 14A. Blot, J.-M. Muller, L. Théry.

    Formal correctness of comparison algorithms between binary64 and decimal64 floating-point numbers, in: Numerical Software Verification, Heidelberg, Germany, Lecture Notes in Computer Science (LNCS), Springer, July 2017, no 10381.

    https://hal.archives-ouvertes.fr/hal-01512294
  • 15C. Cohen, D. Rouhling.

    A Formal Proof in Coq of LaSalle's Invariance Principle, in: Interactive Theorem Proving, Brasilia, Brazil, September 2017. [ DOI : 10.1007/978-3-319-66107-0_10 ]

    https://hal.inria.fr/hal-01612293

National Conferences with Proceedings

  • 16C. Cohen, D. Rouhling.

    A refinement-based approach to large scale reflection for algebra, in: JFLA 2017 - Vingt-huitième Journées Francophones des Langages Applicatifs, Gourette, France, January 2017.

    https://hal.inria.fr/hal-01414881

Internal Reports

  • 17J. Grimm.

    Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers, Inria Sophia Antipolis ; Inria, 2017, no RR-7150, pp. 1-764.

    https://hal.inria.fr/inria-00440786

Other Publications

References in notes
  • 23R. Chen, J.-J. Lévy.

    A Semi-automatic Proof of Strong connectivity, in: 9th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Heidelberg, Germany, July 2017.

    https://hal.inria.fr/hal-01632947
  • 24M. Joldes, V. Popescu, J.-M. Muller.

    Tight and rigourous error bounds for basic building blocks of double-word arithmetic, July 2016, working paper or preprint.

    https://hal.archives-ouvertes.fr/hal-01351529


previous Previous | up Home