CITATION

Inductive methods for proving properties of programs, Communications of the ACM, August 1973 (with Zohar Manna, Jean Vuillemin)