An automated reasoning problem associated with proving claims about programs using Floyd-Hoare inductive assertion methods - Chisholm, G. H.; Smith, B. T.; Wojcik, A. S. (Springer, 1989)
http://dx.doi.org/10.1007/BF00243137
Keywords: SQ-SU