Associé à l'équipe LANDE à l'IRISA.

Domaines d'intérêt

• Méthodes formelles
• Assistants à la preuve
• Logique
• Sémantique des langages de programmation
• Sécurité et Protection de la vie privée

Doctorat

Vérification Formelle de la Plate-forme JavaCard.

Recherche à l'INRIA Sophia Antipolis dans l'équipe Everest.
Diplôme décerné par l'Université de Nice.

Publications

• F. Besson, G. Dufay, T. Jensen. A Formal Model of Access Control for Mobile Interactive Devices. In Proceedings of ESORICS 2006. To appear.
• G. Barthe, G. Dufay. A Tool-Assisted Framework for Certified Bytecode Verification and its Application to JavaCard. Submitted to the Journal on Software Tools for Technology Transfer (STTT).
• G. Barthe, G. Dufay. Formal methods for Smartcard security. Chapter of Foundations of Security Analysis and Design (FOSAD), LNCS 3655, pp 133--177. © Springer-Verlag.
• G. Dufay, A. Felty, S. Matwin. Privacy-Sensitive Information Flow with JML. In Proceedings of the Conference on Automated Deduction (CADE-20), LNAI 3632, pp 116--130. © Springer-Verlag.
• G. Barthe, P. Courtieu, G. Dufay, and S. Melo de Sousa. A Tool-Assisted Specification and Verification of Typed Low-Level Languages. In Journal of Automated Reasoning. To appear.
• G. Barthe, G. Dufay. A Tool-Assisted Framework for Certified Bytecode Verification. In T. Margaria and M. Wermelinger, editors, Proceedings of FASE'04, LNCS 2984, pp 99--113. © Springer-Verlag
• G. Barthe, P. Courtieu, G. Dufay, and S. Melo de Sousa. Tool-Assisted Specification and Verification of the JavaCard Platform. In H. Kirchner and C. Ringeissen, editors, Proceedings of AMAST'02, LNCS 2422, p 41--59. © Springer-Verlag
• G. Dufay. Vérification formelle de la plate-forme JavaCard. Thèse de Doctorat, Université de Nice, 2003.
• G. Barthe, G. Dufay, L. Jakubiec and S. Melo de Sousa. A formal correspondence between offensive and defensive JavaCard virtual machines. In A. Cortesi, editor, Proceedings of VMCAI'02, LNCS 2294, p 32--45. © Springer-Verlag
• G. Barthe, G. Dufay, M. Huisman, and S. Melo de Sousa. Jakarta: a toolset to reason about the JavaCard platform. In I. Attali and T. Jensen, editors, Proceedings of e-SMART'01, LNCS 2140. p 2--18. © Springer-Verlag
• G. Barthe, G. Dufay, L. Jakubiec, B. Serpette, and S. Melo de Sousa. A Formal Executable Semantics of the JavaCard Platform. In D. Sands, editor, Proceedings of ESOP'01, LNCS 2028, p 302--319. © Springer-Verlag
• G. Barthe, G. Dufay, L. Jakubiec, B. Serpette, S. Melo de Sousa and S-W. Yu. Formalization of the JavaCard Virtual Machine in Coq. In S. Drossopoulou et al, editor, Proceedings of FTfJP'00, p 50--56.
• G. Dufay. Formalisation en Coq de la Machine Virtuelle JavaCard. Rapport de DEA, Université Paris VII - Denis Diderot, 2000.
• G. Dufay. Preuve du théorème de Matiyasevich dans le système Coq. Rapport de Travail d'Etude et de Recherche, Université de Paris Sud - Orsay, 1999.