Solving Conditional Linear Recurrences for Program Verification: The Periodic Case

Explore a 15-minute video presentation from OOPSLA1 2023 conference that delves into solving conditional linear recurrences for program verification, focusing on the periodic case. Learn about a novel approach to reasoning about loops in program verification by converting them into sets of recurrences and computing closed-form solutions. Discover the challenges posed by conditional expressions in recurrences and the proposed method for addressing them. Understand the concept of ultimately periodic index sequences and their importance in finding closed-form solutions. Examine the heuristic 'generate and verify' algorithm developed to check ultimate periodicity and compute solutions simultaneously. Gain insights into the implementation of a solver based on this algorithm and its effectiveness in verifying properties of benchmark programs with conditional statements in loops. Compare the performance of this approach to other recurrence-based verification tools. Consider the potential extensions of these results to recurrences with unknown initial values.