Reasoning about Java Classes (Preliminary Report). - Bart Jacobs 001; Joachim van den Berg; Marieke Huisman; Martijn van Berkum (OOPSLA, 1998)

A Type-Theoretic Memory Model for Verification of Sequential Java Programs. - Joachim van den Berg; Marieke Huisman; Bart Jacobs 001; Erik Poll (WADT, 1999)

Specification of the JavaCard API in JML. - Erik Poll; Joachim van den Berg; Bart Jacobs 001 (CARDIS, 2000)

Formal Specification and Verification of JavaCard's Application Identifier Class. - Joachim van den Berg; Bart Jacobs 001; Erik Poll (Java Card Workshop, 2000)

The LOOP Compiler for Java and JML. - Joachim van den Berg; Bart Jacobs 001 (TACAS, 2001)

Formal specification of the JavaCard API in JML: the APDU class. - Erik Poll; Joachim van den Berg; Bart Jacobs 001 (Comput. Networks, 2001)

A case study in class library verification: Java's vector class. - Marieke Huisman; Bart Jacobs 001; Joachim van den Berg (Int. J. Softw. Tools Technol. Transf., 2001)

Specifying and Verifying a Decimal Representation in Java for Smart Cards. - Cees-Bart Breunesse; Bart Jacobs 001; Joachim van den Berg (AMAST, 2002)

Bellcore attack in practice. - Andrey Sidorenko; Joachim van den Berg; Remko Foekema; Michiel Grashuis; Jaap de Vos (IACR Cryptol. ePrint Arch., 2012)