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-app

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.