Guillaume Dufay
Post-doctoral researcher
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.
Contact Information
Guillaume Dufay
IRISA - Projet Lande
Campus de Beaulieu
F-35042 Rennes Cedex
France
Office: D068
E-mail: Guillaume.Dufay@irisa.fr
Phone: +33 2 99 84 74 04
Fax: +33 2 99 84 71 71