No, because you need different strategies to prove the loop case (which you can do with just a sequence of transitions), the halt case (the same) and the use the infinite amount of memory case.
There is no proof that will catch 100% of case 3, (because then you would have a halting oracle). But you can create a program that will halt iff a program halts, or halt iff it loops in finite states or halts. (I could write it, but it just runs real slow). You cannot write the program that halts if another program uses an infinite amount of memory (since then you could build a halting oracle). There are NO halting oracles, not just no efficient halting oracles.
Is that supposed to be weather?