[hun3]

Verified software should satisfy the liveness property; otherwise, an infinite loop that never returns would pass as "correct."

Verifying realtime software goes even further and enforces an upper bound on the maximum number of ticks it takes to complete the algorithm in all cases.