[Dylan16807]

> For example, finding out whether a time-bounded Turing machine outputs 0 all inputs is still undecidable.

Is that a problem? I mean, if you're installing a timeout then haven't you already decided that the answer is "no"?

[fnrslvr]

If the time bound is being put in place in the hopes of being able to automatically analyze the behaviour of the code, then no.

I singled out "outputting 0" on every input because it's among the simplest possible specs you could try try to check with the kind of "very powerful semantic analysis" tool the top-level post was hoping for. In practice you probably want to check a more complex spec -- you want your code to solve a specific problem on whatever input it receives -- but if the "always output 0" spec is impossible to automatically check, then what hope do more relevant specs have?