Solving Recurrence for Program Verification

The Hong Kong University of Science and Technology
Department of Computer Science and Engineering


PhD Thesis Defence


Title: "Solving Recurrence 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. In this thesis, 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 there are possibly infinite number of polynomials 
satisfying some c-finite recurrences for a given loop, 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:                   Friday, 7 June 2024

Time:                   2:00pm - 4:00pm

Venue:                  Room 5501
                        Lifts 25/26

Chairman:               Dr. Ki Ling CHEUNG (ISOM)

Committee Members:      Prof. Fangzhen LIN (Supervisor)
                        Prof. Shing-Chi CHEUNG
                        Dr. Amir GOHARSHADY
                        Dr. Hongce ZHANG (ECE)
                        Prof. Zhiming LIU (SWU)