H. Peter Gumm: Generating Algebraic Laws from Imperative Programs. Theor. Comput. Sci. 217(2): 385-405 (1999)