NASA has released JavaPathFinder. What is JavaPathFinder?? here is an excerpt
"""If you are not familiar with formal methods, this basically means JPF is a Java virtual machine that executes your program not just once (like a normal VM), but theoretically in all possible ways, checking for property violations like deadlocks or unhandled exceptions along all potential execution paths. If it finds an error, JPF reports the whole execution that leads to it. Unlike a normal debugger, JPF keeps track of every step how it got to the defect."""
interesting ... need to figure out where Halting Problem theorem stands ..