Formal Proof of Smart Card Applets Correctness. - Jean-Louis Lanet; Antoine Requet (CARDIS, 1998)

Application of the B formal method to the proof of a type verification algorithm. - Antoine Requet; Ludovic Casset; Gilles Grimaud (HASE, 2000)

Embedding Formally Proved Code in a Smart Card: Converting B to C. - Antoine Requet; Gaëlle Bossu (ICFEM, 2000)

Formal Development of an Embedded Verifier for Java Card Byte Code. - Ludovic Casset; Lilian Burdy; Antoine Requet (DSN, 2002)

Adaptable Translator of B Specifications to Embedded C Programs. - Didier Bert; Sylvain Boulmé; Marie-Laure Potet; Antoine Requet; Laurent Voisin (FME, 2003)

Java Applet Correctness: A Developer-Oriented Approach. - Lilian Burdy; Antoine Requet; Jean-Louis Lanet (FME, 2003)

Java Card Code Generation from B Specifications. - Bruno Tatibouët; Antoine Requet; Jean-Christophe Voisinet; Ahmed Hammad (ICFEM, 2003)

Extending B with Control Flow Breaks. - Lilian Burdy; Antoine Requet (ZB, 2003)

A B model for ensuring soundness of a large subset of the Java Card virtual machine. - Antoine Requet (Sci. Comput. Program., 2003)

Développement formel d'un vérifieur embarqué de byte-code Java. - Lilian Burdy; Ludovic Casset; Antoine Requet (Tech. Sci. Informatiques, 2003)

JACK - A Tool for Validation of Security and Behaviour of Java Applications. - Gilles Barthe; Lilian Burdy; Julien Charles; Benjamin Grégoire; Marieke Huisman; Jean-Louis Lanet; Mariela Pavlova; Antoine Requet (FMCO, 2006)

BART: A Tool for Automatic Refinement. - Antoine Requet (ABZ, 2008)

Formal Proofs for the NYCT Line 7 (Flushing) Modernization Project. - Denis Sabatier; Lilian Burdy; Antoine Requet; Jérôme Guéry (ABZ, 2012)