Using PVS to Prove a Z Refinement: A Case Study. - David W. J. Stringer-Calvert; Susan Stepney; Ian Wand (FME, 1997)