F.  Giannotti and Hermenegildo, M. V., ?A Technique for Recursive Invariance Detection and Selective Program Specification?, in PLILP, 1991, pp. 323-334.