[dllthomas]

In principle it reduces to the halting problem, but given that the domain we're discussing is real-time systems, you'd better already be dealing with programs that you know will halt (in the sense of producing an answer) in not just a finite amount of time but even below some particular bound! Once you've constrained yourself to those programs, you may well be able to get a general result... but as others have noted, really what we want is results about specific programs, and the halting problem has nothing to say there.

I don't know that there exists tooling to construct these proofs, beyond general proof-constructing support, but I'm not working in hard-realtime environments so I'm sure I'm not aware of everything going on either.