D.  Pedreschi, ?A Proof Method for Runtime Properties of Prolog Programs?, in ICLP, 1994, pp. 584-598.