kleendr12

3 ms·

1. 1.▲
   by kleendr12 6y ago

   I'm not quite sure I follow your comment. If the program never terminates then it will loop forever and potentially freeze the machine depending from where it is invoked in the kernel. Example of loops that can be detected to terminate
2. 2.▲
   by kleendr12 6y ago

   When there's no loop bound it cannot prove termination, see halting problem. Goal is to avoid getting an infinite loop and then freezing the kernel of course.
3. 3.▲
   by kleendr12 6y ago

   Loops must be bounded, that means, the verifier must be able to see that the loop will eventually terminate based on the condition. The verifier will simulate all iterations of the loop and as such it is limited by the verifier complexity,