3 ms·

The halting problem is just an example. The real concern is that any "nontrivial" program property is also undecidable (see Rice's Theorem)

• Animats 11y ago
  That's incorrect. Rice's theorem only says that it is possible to construct programs for which "nontrivial" program properties are undecidable. But you don't have to construct undecidable programs. In fact, you have to work at it to write a useful but formally undecidable program. (Also, you need infinite memory to get theoretical undecidability from a deterministic system. With finite memory you eventually have to halt or repeat a state.) The people behind the Microsoft Static Driver Verifier say that they are unable to decide if a program is safe to be a kernel driver about 4% of the time. This is grounds for rejecting the driver. If your kernel driver is anywhere near the limits of formal decidability, it shouldn't be in the kernel. Typically, you fix undecidability by adding loop counters or checking. If you have some complex algorithm where termination is hard to prove, adding a loop counter and an iteration limit will guarantee termination. (This comes up as a practical matter in floating point work. There are algorithms which are guaranteed to terminate on real numbers, but not on finite-precision floating point numbers. One example I've run into is GJK, used in collision detection.) Undecidability is just not a problem in real program verification.
  • ufo 11y ago
    I wasn't trying to imply that formal verification can't work around undecidability in practice. But you are correct in saying that you can often avoid undecidability by restricting yourself to certain idioms, type systems, etc.