Abstract Loops are inductive constructs, which make them difficult to analyze and verify in general. One approach is to represent the inductive behaviors of the program variables in a loop by recurrences and try to solve them for closed-form solutions. These solutions can then be used to generate invariants or directly fed into an SMT-based verifier. One problem with this approach is that if a loop contains nondeterministic choices or complex operations such as non-linear assignments, then recurrences for program variables may not exist or may have no closed-form solutions. In such cases, an alternative is to generate recurrences for expressions, and there has been recent work along this line. In this paper, we further work in this direction and propose a template-based method for extracting polynomial expressions that satisfy some c-finite recurrences. While in general there are possibly infinitely many such polynomials for a given loop, we show that the desired polynomials form a finite union of vector spaces. We propose an algorithm for computing the bases of the vector spaces, and identify two cases where the bases can be computed efficiently. To demonstrate the usefulness of our results, we implemented a prototype system based on one of the special cases, and integrated it into an SMT-based verifier. Our experimental results show that the new verifier can now verify programs with non-linear properties.

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.