Dr. Grigory Fedyukovich has a paper accepted at the 2025 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). PLDI is a flagship conference in programming languages. The paper, titled “Exact Loop Bound Analysis”, is authored by Dr. Grigory Fedyukovich and his PhD student Daniel Riley.
The paper presents ELBA, a novel tool for exact loop bound analysis, a largely unexplored area in program analysis. While many techniques can find an upper or lower bound for loops, determining an exact bound has remained a significant challenge due to the variability of program inputs. ELBA introduces a new approach using precondition synthesis to compute precise loop bounds. For a given program, the tool synthesizes a function that, when applied to the initial values of program variables, yields an exact bound for the loop’s execution. The approach utilizes abductive inference to find a description of each possible loop execution and applies a bound to each of the cases. The synthesized bound is then sent to a verifier, ensuring its correctness. The evaluation on a set of challenging single-loop benchmarks demonstrates ELBA’s effectiveness when compared against state-of-the-art bound and termination analysis tools.