Termination analysis of floating-point loops with bounded exponent

[Cloerkes, Daniel]

Dear FPBench community,

first of all, many thanks to Zachary Tatlock for adding me to the mailing list.

I am writing to ask for pointers regarding the termination analysis of linear loops over floating-point numbers, in particular in the standard setting of bounded exponents (e.g. IEEE-754 single precision).

In recent years, I have developed a technique to decide termination for such loops. The approach combines a box abstraction with ranking functions tailored to floating-point semantics. While the state space is finite due to the bounded exponent, exhaustive enumeration is clearly infeasible in practice. Instead, the method reasons over larger, box-shaped regions of the state space, avoiding both explicit simulation and pointwise analysis.

I would be very grateful for any guidance on the following questions:

1. Are you aware of research groups or publications that specifically address termination of floating-point programs in the bounded-exponent setting?

2. Are there existing implementations or tools (possibly as part of larger verification frameworks) that support or approximate such analyses, and could serve as a basis for comparison or benchmarking?

I appreciate any pointers or references you may be able to share.

Thank you very much for your time.

Kind regards,
Daniel Cloerkes