Ranking Function Generation with LLMs for Termination.

arXiv:2610.35523v1 Announce Type: cross Abstract: Ranking functions are a fundamental technique for proving loop termination, but constructing them manually is challenging and requires substantial expertise. We propose RAINFALL, a neuro-symbolic framework whic