Termination analysis with interpolation-based transition invariant generation
A new termination analysis approach based on the generation of well-founded transition invariants that leverages Craig interpolation for transition invariant generation, capturing the structural reasons for termination.