3 ms·
They overapproximate. This means that may say something probably doesn't terminate even if it terminates. The idea is that if it says it terminates, then there
by veselin 6y ago
They overapproximate. This means that may say something probably doesn't terminate even if it terminates. The idea is that if it says it terminates, then there is a proof it does.
- zomglings 6y agoDo they know beforehand a value of N so that the proofs have depth < N?
- lou1306 6y agoNot necessarily. For instance, CBMC has been participating in the Termination category with an approach based on Bounded model checking, an underapproximation technique. Thus, they always produce correct result, but their analysis might not terminate (or may terminate with an "unknown" verdict).