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?
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).
> 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.