Jakarta: A Toolset for Reasoning about JavaCard. - Gilles Barthe; Guillaume Dufay; Marieke Huisman; Simão Melo de Sousa (E-smart, 2001)

A Formal Executable Semantics of the JavaCard Platform. - Gilles Barthe; Guillaume Dufay; Line Jakubiec; Bernard P. Serpette; Simão Melo de Sousa (ESOP, 2001)

Tool-Assisted Specification and Verification of the JavaCard Platform. - Gilles Barthe; Pierre Courtieu; Guillaume Dufay; Simão Melo de Sousa (AMAST, 2002)

A Formal Correspondence between Offensive and Defensive JavaCard Virtual Machines. - Gilles Barthe; Guillaume Dufay; Line Jakubiec; Simão Melo de Sousa (VMCAI, 2002)

A Tool-Assisted Framework for Certified Bytecode Verification. - Gilles Barthe; Guillaume Dufay (FASE, 2004)

Privacy-Sensitive Information Flow with JML. - Guillaume Dufay; Amy P. Felty; Stan Matwin (CADE, 2005)

Formal Methods for Smartcard Security. - Gilles Barthe; Guillaume Dufay (FOSAD, 2005)

Tool-Assisted Specification and Verification of Typed Low-Level Languages. - Gilles Barthe; Pierre Courtieu; Guillaume Dufay; Simão Melo de Sousa (J. Autom. Reason., 2005)

A Formal Model of Access Control for Mobile Interactive Devices. - Frédéric Besson; Guillaume Dufay; Thomas P. Jensen (ESORICS, 2006)

Verifying resource access control on mobile interactive devices. - Frédéric Besson; Guillaume Dufay; Thomas P. Jensen; David Pichardie (J. Comput. Secur., 2010)