Checking JML Specifications with B Machines. - Fabrice Bouquet; Frédéric Dadeau; Julien Groslambert (ZB, 2005)

JAG: JML Annotation Generation for Verifying Temporal Properties - Alain Giorgetti; Julien Groslambert (FASE, 2006)

Safety Property Driven Test Generation from. - Fabrice Bouquet; Frédéric Dadeau; Julien Groslambert; Jacques Julliand (FATES/RV, 2006)

JML-based verification of liveness properties on a class in isolation. - Julien Groslambert; Jacques Julliand; Olga Kouchnarenko (SAVCBS@FSE, 2006)

JML2B: Checking JML Specifications with B Machines. - Fabrice Bouquet; Frédéric Dadeau; Julien Groslambert (B, 2007)

Verification of LTL on B Event Systems. - Julien Groslambert (B, 2007)

A. - Julien Groslambert (B, 2007)

Verification of class liveness properties with java modelling language. - Alain Giorgetti; Julien Groslambert; Jacques Julliand; Olga Kouchnarenko (IET Softw., 2008)