JML: A Notation for Detailed Design. - Gary T. Leavens; Albert L. Baker; Clyde Ruby (Behavioral Specifications of Businesses and Systems, 1999)

JML (poster session): notations and tools supporting detailed design in Java. - Gary T. Leavens; Clyde Ruby; K. Rustan M. Leino; Erik Poll; Bart Jacobs 001 (OOPSLA Addendum, 2000)

Safely creating correct subclasses without seeing superclass code. - Clyde Ruby (OOPSLA Addendum, 2000)

Safely creating correct subclasses without seeing superclass code. - Clyde Ruby; Gary T. Leavens (OOPSLA, 2000)

How the Design of JML Accomodates Both Runtime Assertion Checking and Formal Verification. - Gary T. Leavens; Yoonsik Cheon; Curtis Clifton; Clyde Ruby; David R. Cok (FMCO, 2002)

How the design of JML accommodates both runtime assertion checking and formal verification. - Gary T. Leavens; Yoonsik Cheon; Curtis Clifton; Clyde Ruby; David R. Cok (Sci. Comput. Program., 2005)

Preliminary design of JML: a behavioral interface specification language for java. - Gary T. Leavens; Albert L. Baker; Clyde Ruby (ACM SIGSOFT Softw. Eng. Notes, 2006)