All non-trivial semantic properties of a program are Undecidable.
Theorem
For any interesting property of the behavior of a program, it is impossible to write an analysis that can decide for every program whether holds for .
All non-trivial semantic properties of a program are Undecidable.
For any interesting property Pr of the behavior of a program, it is impossible to write an analysis that can decide for every program p whether Pr holds for p.