Recurrence Solving and Its Application in Software Verification and Analysis

PhD Qualifying Examination


Title: "Recurrence Solving and Its Application in Software Verification and 
Analysis"

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. Recurrence 
solving also plays an important role in software analysis. 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, recurrence 
solving techniques have a great impact on the analysis of loops. In this 
survey, we first review three approaches for recurrence solving. Examples for 
demonstrating their usefulness are given. The comparison between these 
approaches is also discussed. Then, two frameworks relying heavily on 
recurrence solving for software verification are introduced. Brief descriptions 
of implementations based on these frameworks are also included. Finally, we 
conclude this survey by discussing the limitations of these recurrence solving 
techniques. Examples showing the difficulties faced by the implementations 
based on these two frameworks are given.


Date:			Thursday, 24 June 2021

Time:                  	3:00pm - 5:00pm

Zoom meeting:
https://hkust.zoom.us/j/98924145254?pwd=Tm9rc3lIUVF3SmlxNnhaMnNpSTlydz09

Committee Members:	Prof. Fangzhen Lin (Supervisor)
 			Dr. Shuai Wang (Chairperson)
 			Dr. Amir Goharshady
 			Dr. Lionel Parreaux


**** ALL are Welcome ****