[ThreeFx]

Not really, because for undecidable problems semidecidability can only hold one-way. If it held in both ways then the language would be decidable.

Take the Halting program for example: For a program p which halts, you can determine whether it will halt in finite time (because by definition it halts). However, there is no semidecidable algorithm for "this program runs infinitely long".

[thaumasiotes]

I don't understand what you're trying to say. What are you contradicting with "Not really"? The claim above you is "by this definition, program incorrectness isn't semidecidable either". You're saying that it is?