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.