Associated with the Lande research group at IRISA.

Research Interests

• Formal methods
• Proof assistants
• Logic
• Programming languages semantics
• Security and Privacy

Ph. D. Thesis

Formal Verification of the JavaCard Platform.

Research at INRIA Sophia Antipolis in the Everest team.
Degree from the University of 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. PhD Thesis, 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. Master Thesis, 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.