Implicit induction techniques for the verification of PIM : a transformational toolkit for compilers
Implicit induction techniques for the verification of PIM : a transformational toolkit for compilers / D. Naidich, T.B. Dinesh