Leveraging Graph Decompositions for Faster Program Analysis and Compiler Optimization

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


PhD Thesis Defence


Title: "Leveraging Graph Decompositions for Faster Program Analysis and 
Compiler Optimization"

By

Mr. Kerim KOCHEKOV


Abstract:

Parameterized complexity offers a principled way to tackle computationally 
hard problems by exploiting structural properties of inputs. This thesis 
applies this framework to program analysis, formal verification, and compiler 
optimization, focusing on graph-based representations of programs such as 
control-flow and call graphs.

On the program analysis side, we leverage structural parameters such as 
treewidth and treedepth to design fixed-parameter tractable algorithms within 
the Algebraic Program Analysis (APA) framework. We present an efficient 
on-demand APA approach that answers multiple source-target queries by 
combining tree decompositions with centroid decompositions, avoiding the 
treewidth blowup present in prior work and significantly improving runtime 
performance.

On the compiler optimization side, we study function merging for binary-size 
reduction. We introduce a generalized formulation that allows 
semantics-preserving reordering of branches, enabling more flexible matching 
between functions. While this generalization makes the problem NP-hard, we 
analyze it using parameterized complexity and identify key parameters, 
including branching factor and nesting depth, that govern tractability.

Extending our structural approach to formal verification, we bridge the gap in 
SAT-based program analysis between theoretically efficient dynamic programming 
and practically fast conflict-driven clause learning (CDCL). By proving that 
control-flow graphs of structured programs possess bounded treedepth, we 
introduce a novel treedepth-guided CDCL algorithm. This hybrid method achieves 
both practical efficiency and worst-case runtime guarantees that are linear in 
instance size and exponential only in treedepth.

Overall, this thesis demonstrates how exploiting structural parameters enables 
efficient algorithms across program analysis, verification, and compiler 
optimization, bridging theory and practical performance improvements.


Date:                   Friday, 18 September 2026

Time:                   3:00pm - 4:00pm

Venue:                  Room 3494
                        Lifts 25/26

Chairman:               Prof. Hai ZHANG (MATH)

Committee Members:      Dr. Jiasi SHEN (Supervisor)
                        Dr. Amir GOHARSHADY (Co-supervisor, University of Oxford)
                        Dr. Sunil ARYA
                        Dr. Mingxun ZHOU
                        Dr. Maximilian NITZSCHNER (MATH)
                        Prof. Sandip DAS (Indian Statistical Institute)