4 ms·

Termination competitions seem fascinating. Are they restricted to certain subclasses of programs where the Halting Problem is solvable? Or are they more focus

Termination competitions seem fascinating. Are they restricted to certain subclasses of programs where the Halting Problem is solvable? Or are they more focused on bounded termination - Will this general program terminate in at most N steps? Are there techniques that help answer this question in compressed time?

veselin 7y 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 7y ago
  Do they know beforehand a value of N so that the proofs have depth < N?
- lou1306 7y ago
  Not 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).
lou1306 7y ago
There is no general algorithm to determine termination. You can still write an algorithm that gives correct answers, but may not terminate (sound), or one that always terminates but might produce wrong answers (complete). A termination analyzer for, say, C programs is either one of the other. Anyway, SV-COMP's benchmarks are all available at [1]: Termination benchmarks are within the eponymous directories, so feel free to take a look! [1] https://github.com/sosy-lab/sv-benchmarks/tree/master/c https://github.com/sosy-lab/sv-benchmarks/tree/master/c
- zomglings 7y ago
  Thanks for the link (looking at it now), and for the terminology (sound, complete). The trivial algorithm to determine termination is to just run the code. This algorithm is sound but not complete, and is not interesting from the point of view of a termination competition. Very curious about complete but unsound approaches. First instinct is to just determine some rules that allow you to prune paths in the control flow of a program (e.g. prune away bounded loops). This doesn't help with recursion, though. If we were dealing with recursive functions with constrained argument types, I can see rules like "for two calls, integer argument is moving closer to base case" being effective. Generalizing this still feels like it would be magical to me (which means I don't understand it at all).
  - lou1306 7y ago
    You're welcome. It's always nice to see HN talk about program verification! > Very curious about complete but unsound approaches A common approach is over-approximation, i.e. you create a model of the program whose set of traces is a superset of the actual traces. If that model is terminating, then the program also is. Otherwise, you cannot draw any conclusion (as the non-terminating traces in the model might be spurious). Some examples of over-approximating techniques are abstract interpretation and predicate abstraction.

veselin 7y 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 7y ago
Do they know beforehand a value of N so that the proofs have depth < N?
lou1306 7y ago
Not 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).

lou1306 7y ago

There is no general algorithm to determine termination. You can still write an algorithm that gives correct answers, but may not terminate (sound), or one that always terminates but might produce wrong answers (complete). A termination analyzer for, say, C programs is either one of the other. Anyway, SV-COMP's benchmarks are all available at [1]: Termination benchmarks are within the eponymous directories, so feel free to take a look! [1] https://github.com/sosy-lab/sv-benchmarks/tree/master/c https://github.com/sosy-lab/sv-benchmarks/tree/master/c

zomglings 7y ago
Thanks for the link (looking at it now), and for the terminology (sound, complete). The trivial algorithm to determine termination is to just run the code. This algorithm is sound but not complete, and is not interesting from the point of view of a termination competition. Very curious about complete but unsound approaches. First instinct is to just determine some rules that allow you to prune paths in the control flow of a program (e.g. prune away bounded loops). This doesn't help with recursion, though. If we were dealing with recursive functions with constrained argument types, I can see rules like "for two calls, integer argument is moving closer to base case" being effective. Generalizing this still feels like it would be magical to me (which means I don't understand it at all).
- lou1306 7y ago
  You're welcome. It's always nice to see HN talk about program verification! > Very curious about complete but unsound approaches A common approach is over-approximation, i.e. you create a model of the program whose set of traces is a superset of the actual traces. If that model is terminating, then the program also is. Otherwise, you cannot draw any conclusion (as the non-terminating traces in the model might be spurious). Some examples of over-approximating techniques are abstract interpretation and predicate abstraction.