The Halting Problem
described by Alan Turing
in 1936 states that is impossible to come up with a general
algorithm that can compute if a given algorithm will terminate (for all possible input pairs). In other words, the only way to generally determine how a program will behave is to execute it, and this may not give you a definite decision either (just because an algorithm seems to be in a loop for example, doesn't automatically imply that it will never terminate at a later stage). The keyword here is general
(it may be possible to tell if a particular instance of an algorithm will terminate).
There's another problem with the halting problem argument. The validity of the proof depends on hypothetical computers with an infinite amount of storage. Any machine with finite storage can be analyzed by some machine with a larger finite amount of storage.
Another specific (i.e. non-general) case is the Java bytecode verifier. It checks compiled Java language progams to see if they meet a set of security criteria (that they don't underflow or overflow the stack, that they don't do some clever stack shenanigans to perform an illegal type conversion and thus break the type-dependent security, and so forth).
As with your other examples, a general bytecode verifier isn't decidable; but the Java verifier isn't a general verifier - it's only designed to verify bytecode sequences that meet a collection of additional criteria, criteria that the Java compiler agrees to meet. With these restrictions, the resulting programs are deterministically verifiable. "Ah", you might say, "but I can hand-craft a bytecode sequence that the compiler wouldn't, and I'd trick the verifier". That doesn't work: the verifier is particularly paranoic - if it sees a bytecode sequence that doesn't meet those additional criteria (stuff like branches into the middle of control structures) it barfs and rejects the program. Technically by doing that it's "wrong" - most of the bytecode sequences it will encounter will be valid and quite harmless, so (if our goal were to produce a completely correct verifier that accepted all good code and rejected all bad) we could call that a bug. But the goal isn't that - it's to prevent malformed sequences being approved, and it achieves that.
There's more in "Programming for the Java™ Virtual Machine" (Safari link)