Solving Recurrences for Program Verification

PhD Thesis Proposal Defence


Title: "Solving Recurrences for Program Verification"

By

Mr. Chenglin WANG


Abstract:

Recurrence relations appear frequently in computer science. For example, to 
analyze the complexity of an algorithm, one may first establish a recurrence 
relation for the complexity and solve it to obtain the result. Solving 
recurrences also plays an important role in software analysis and verification. 
Loop is one of the important constructs in modern programming languages. The 
behavior of a loop can be naturally characterized by a set of recurrences. 
Therefore, powerful recurrence solving techniques have a great impact on the 
loop analysis. Existing algebra systems (e.g., Mathematica, SymPy) are only 
capable of solving non-conditional recurrences, while conditional ones arise 
due to nested branches in loops. To make recurrence analysis more powerful in 
program verification, we propose a method for solving conditional linear 
recurrences and a method for finding interesting expressions that satisfy some 
solvable recurrences.

First, we take a step towards solving conditional recurrences, which arise when 
a loop body contains nested conditional branches. 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 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. Based on this result, algorithm for 
solving conditional linear recurrence with unknown initial values is proposed.

Second, recurrences for program variables may not exist or have no closed-form 
solutions if loop body contains nondeterministic branches or complex operations 
(e.g., polynomial assignments). In such cases, an alternative is to generate 
recurrences for expressions, and there have been recent works along this line. 
we further work in this direction and propose a template-based method for 
extracting polynomial expressions that satisfy some c-finite recurrences. We 
show that computationally, this amounts to solving a system of quadratic 
equations. While in general these quadratic equations may have infinite 
solutions, we show that the desired polynomials form a finite union of vector 
spaces. An algorithm is proposed for computing the bases of the vector spaces 
and identify two cases where the bases can be computed efficiently.

Finally, we implemented a prototype tool based on these two works, and our 
experiments show that a straightforward program verifier based on our solver 
together with the SMT solver Z3 is effective in verifying properties of many 
benchmark programs that contain conditional statements and polynomial 
assignments in their loops and compares favorably to other verification tools.


Date:                   Tuesday, 23 April 2024

Time:                   9:30am - 11:00am

Venue:                  Room 4472
                        Lifts 25/26

Committee Members:      Prof. Fangzhen Lin (Supervisor)
                        Dr. Jiasi Shen (Chairperson)
                        Dr. Amir Goharshady
                        Prof. Ke Yi