Solving Conditional Linear Recurrences for Program Verification: The Periodic Case

In program verification, one method for reasoning about loops is to convert them into sets of recurrences, and then try to solve these recurrences by computing their closed-form solutions. While there are solvers for computing closed-form solutions to these recurrences, their capabilities are limited when the recurrences have conditional expressions, which arise when the body of a loop contains conditional statements. In this paper, we take a step towards solving these recurrences. Specifically, we consider what we call conditional linear recurrences and show that given such a recurrence and an initial value, if the index sequence generated by the recurrence on the initial value is what we call ultimately periodic, then it has a closed-form solution. However, checking whether such a sequence is ultimately periodic is undecidable so we propose a heuristic "generate and verify" algorithm for checking the ultimate periodicity of the sequence and computing closed-form solutions at the same time. We implemented a solver based on this algorithm, and our experiments show that a straightforward program verifier based on our solver and using the SMT solver Z3 is effective in verifying properties of many benchmark programs that contain conditional statements in their loops, and compares favorably to other recurrence-based verification tools. Finally, we also consider extending our results to computing closed-form solutions of recurrences with unknown initial values.