Anticipating program crashes

I'm working on a program that should be able to tell if any program I run on my computer will crash.

Presumably it's possible to read in the machine code, build a model of the potential code paths, test each code path for behavior under standard and boundary conditions, map out the conditions that result in unhandled exceptions, and then trace all those steps backward to generate the required set up inputs and conditions that would trigger the exceptional code path to be taken. It's like using a fuzzing debugger, only more methodical. Sure it's a lot of work, but it should go very quickly on modern hardware.

A coworker said t开发者_高级运维hat what I'm trying to do is fundamentally impossible. That seems a little extreme to me. Given Moore's law curve of technology development, computing power that is out of reach will eventually become reality -- eventually. It would seem a bit of an overstatement to suggest that such a thing would remain forever impossible.

Why can't this be done?

Here is a program :

accept integer i greater than 2
loop with k from 2 to 2*i
  is k prime?
    is 2*i-k prime?
      exit safely
end loop
do something nasty.

If you trace the input that cause this program to do something nasty, you have solved Goldbach's conjecture. You can collect a Fields medal along with your Nobel prize.

This said, it is possible to verify that some programs do not do anything nasty. I and others are working on a framework in which you can do just that, using various techniques. Some examples:

This compression library could exhibit a memory error with input size 20, output size 40, but now it won't.

This binary search could fail, but now it won't.

This is one of the Holy Grails of computing and mathematics, known as the Entscheidungsproblem. You're not going to solve it. The brightest minds in both fields spent many years on it, and proved that it could not be solved. When nbt and Pascal Cuoq said you'd win the Nobel and Fields for doing so, they really meant it.

Presumably it's possible to read in the machine code, build a model of the potential code paths, test each code path for behavior under standard and boundary conditions, map out the conditions that result in unhandled exceptions, and then trace all those steps backward to generate the required set up inputs and conditions that would trigger the exceptional code path to be taken.

Yes, it is possible, despite what the theory folks say. There are multiple companies selling products that do exactly what you are describing, among them Vericode, Coverity, Fortify, Klocwork, and Grammatech.

The theory says this is impossible, assuming you want something that is both sound and complete. In practice, you can drop both soundness and completeness, so long as your false positive rate isn't too bad, and you will have customers lining up to buy your product.

Once you drop soundness and completeness, the impossibility theorems no longer hold, and you move into something much more like engineering than theory.

Edit, for Alex's comment
I will take the mathematicians shortcut, and say that since the original question is "Is it possible" the existence of several viable commercial products proves the answer is "yes". The economic dependencies that might be created by using commercial software are beyond the scope of the original question.