The Knuth-Bendix Completion Algorithm and Its Specification in Z. - Alf Smith (Z User Workshop, 1989)

On Recursive Free Types in Z. - Alf Smith (Z User Workshop, 1991)

Don't Verify, Abstract! - Colin O'Halloran; Alf Smith (ASE, 1998)

Verification of Picture Generated Code. - Colin O'Halloran; Alf Smith (ASE, 1999)

ClawZ: Control Laws in Z. - R. D. Arthan; P. Caseley; Colin O'Halloran; Alf Smith (ICFEM, 2000)