Lambda the Ultimate

Is there any literature that investigates the abilities and limitations of Program Proving software in relationship to the halting problem? It seems like there is a relationship there that would warrant investigation, but I wasn't aware of where to find literature on the subject.

Thanks!