University of Oxford & Max Planck Institute Joint Program
Doctor of Philosophy, Computer Science — Sep 2025 – Present
Supervisor(s): Prof. Amir Goharshady, Prof. Rupak Majumdar
Hi — I’m
Xuran Cai
Computer Science PhD student in the Oxford–Max Planck joint PhD program (2025–present). On the Oxford side, I am a member of Hertford College at the University of Oxford, supervised by Prof. Amir Goharshady. On the Max Planck side, I am at the Max Planck Institute for Software Systems (MPI-SWS), supervised by Prof. Rupak Majumdar. My research focuses on applications of graph theory in computer science and, more broadly, on optimization and verification problems in theoretical computer science.
Current: Oxford–Max Planck joint PhD (Computer Science) — 2025–Present
Education
Hong Kong University of Science and Technology
MPhil, Computer Science & Engineering — 2023–2025
Supervisor(s): Prof. Amir Goharshady, Prof. Jiasi Shen
University of Wisconsin–Madison
B.Sc., Computer Science & Mathematics — 2019–2023
GPA: 3.86/4.0 — Graduated with Distinction
Research
My research centers on applications of graph theory in computer science and, more broadly, on optimization and verification problems in theoretical computer science. I am funded by a scholarship from the University of Oxford and a researcher salary from the Max Planck Institute for Software Systems (MPI-SWS). Selected publications and manuscripts are listed below; for a complete record, please see my CV or Google Scholar profile.
Ongoing Research
Solving MDPs with an Error Budget
VerificationUnder review at TACAS'27
Hub-Certificate Proofs for ARX-32 Impossible Differentials
VerificationOngoing
SPL-Decompositions for Profile Inference
OptimizationOngoing
Local Certificates for Shared-Resource Admission Controllers
VerificationOngoing
Selected Publications & Manuscripts
Venue rank, higher → lower:
CORE
A*
A
B
C
CCF
A
B
C
Extending Programmable Blockchain Protocols to Enable and Incentivize Parallel Execution of Smart Contracts
OptimizationSep 2026 — MARBLE'26
Authors: T. Barakbayeva, X. Cai, Z. Cai, A.K. Goharshady
Modern nodes on blockchain networks are typically deployed on multi-core hardware. However, in current blockchain consensus protocols, such as those of Cardano and Ethereum, the nodes have to process the transactions in each block in a sequential manner according to the order specified by the producer, leaving their parallel computational resources underutilized. The main challenge in parallel execution comes from transaction dependencies, e.g. different functions reading from and writing to the same location in a contract’s storage. This makes safe concurrent execution difficult. A node that wishes to use concurrency currently has to pay the overhead of finding a suitable concurrent schedule. More importantly, since these protocols do not assume parallel execution, the amount of computation performed in each block has to be limited by the sequential computational power of the weakest nodes. Thus, any benefit obtained from parallelization does not translate to shorter block times or higher throughput.
In this work, we solve these problems by presenting two novel parallel blockchain protocols that extend the standard eUTXO and account-based models and provide native support for parallelization. In our protocols, the burden of finding an efficient concurrent schedule is shifted to the producers, who typically have much more computational power than the nodes. Moreover, the producers are incentivized to effectively utilize parallelization and minimize the total runtime (makespan). As a result, the computational limits in each block and the times between any two consecutive blocks can be set according to the parallel (rather than sequential) computational power of our nodes, leading to significant improvements in throughput. The full version of the paper is available at HAL hal-05724231.
Polynomial Invariant Generation for Floating Point Programs
VerificationJul 2026 — CAV'26 CORE A*CCF-A
Authors: X. Cai, L. Chen, H. Fu
In numeric-intensive computations, it is well known that the execution of floating-point programs is imprecise as floating-point arithmetic incurs round-off errors. Although round-off errors are small for a single floating-point operation, the aggregation of such errors may be dramatic and cause catastrophic program failures. Therefore, to ensure the correctness of floating-point programs, round-off error needs to be carefully taken into account. In this work, we consider polynomial invariant generation for floating-point programs, aiming at generating tight invariants under the perturbation of round-off errors. Our contribution is a novel framework for applying polynomial constraint solving to address the invariant generation problem, which is also the first polynomial constraint solving based approach that handles floating-point errors to our best knowledge. In our framework, we propose a novel combination of round-off error analysis and polynomial constraint solving, aiming to circumvent the cost of handling a large number of error variables in the floating-point model. Experimental results over a variety of challenging benchmarks show that our framework outperforms SOTA approaches in both time efficiency and the precision of generated invariants.
Series-Parallel-Loop Decompositions of Control-flow Graphs
OptimizationFeb 2026 — JSA'26 CCF-B
Authors: X. Cai, A.K. Goharshady, S. Hitarth, C.K. Lam
Control-flow graphs (CFGs) of structured programs are well known to exhibit strong sparsity properties. Traditionally, this sparsity has been modeled using graph parameters such as treewidth and pathwidth, enabling the development of faster parameterized algorithms for tasks in compiler optimization, model checking, and program analysis. However, these parameters only approximate the structural constraints of CFGs: although every structured CFG has treewidth at most 7, many graphs with treewidth at most 7 cannot arise as CFGs. As a result, existing parameterized techniques are optimized for a substantially broader class of graphs than those encountered in practice.
In this work, we introduce a new grammar-based decomposition framework that characterizes exactly the class of control-flow graphs generated by structured programs. Our decomposition is intuitive, mirrors the syntactic structure of programs, and remains fully compatible with the dynamic-programming paradigm of treewidth-based methods. Using this framework, we design improved algorithms for two classical compiler optimization problems: Register Allocation and Lifetime-Optimal Speculative Partial Redundancy Elimination (LOSPRE). Extensive experimental evaluation demonstrates significant performance improvements over previous state-of-the-art approaches, highlighting the benefits of using decompositions tailored specifically to CFGs.
Efficient Algorithms for Partial Constraint Satisfaction Problems over Control-flow Graphs
OptimizationDec 2025 — SETTA'25 CCF-C
Authors: X. Cai, A.K. Goharshady
In this work, we focus on the Partial Constraint Satisfaction Problem (PCSP) over control-flow graphs (CFGs) of programs. PCSP serves as a generalization of the well-known Constraint Satisfaction Problem (CSP). In the CSP framework, we define a set of variables, a set of constraints, and a finite domain D that encompasses all possible values for each variable. The objective is to assign a value to each variable in such a way that all constraints are satisfied. In the graph variant of CSP, an underlying graph is considered and we have one variable corresponding to each vertex of the graph and one or several constraints corresponding to each edge. In PCSPs, we allow for certain constraints to be violated at a specified cost, aiming to find a solution that minimizes the total cost. Numerous classical compiler optimization tasks can be framed as PCSPs over control-flow graphs. Examples include Register Allocation, Lifetime-optimal Speculative Partial Redundancy Elimination (LOSPRE), and Optimal Placement of Bank Selection Instructions. On the other hand, it is well-known that control-flow graphs of structured programs are sparse and decomposable in a variety of ways. In this work, we rely on the Series-Parallel-Loop (SPL) decompositions as introduced by [7]. Our main contribution is a general algorithm for PCSPs over SPL graphs with a time complexity of O(|G| · |D|6), where |G| represents the size of the control-flow graph. Note that for any fixed domain D, this yields a linear-time solution. Our algorithm can be seen as a generalization and unification of previous SPL-based approaches for register allocation and LOSPRE. In addition, we provide experimental results over another classical PCSP task, i.e. Optimal Bank Selection, achieving runtimes four times better than the previous state of the art.
Enhancing Compiler Optimization Efficiency through Grammatical Decompositions of Control-Flow Graphs
OptimizationJul 2025 — MPhil Thesis, HKUST Thesis
Author: X. Cai
Compiler optimizations, including register allocation and Lifetime-optimal Speculative Partial Redundancy Elimination (LOSPRE), present inherent complexities that are often addressed through tree decomposition algorithms. However, these approaches often neglect important sparsity aspects of Control Flow Graphs (CFGs) and incur significant computational costs during decomposition, leading to inefficiencies in compiler optimization tasks. This thesis introduces the SPL (Series-Parallel-Loop) decomposition, a novel framework that we have developed to provide optimal solutions to these challenges. A significant contribution of this research is the formulation of a general solution for Partial Constraint Satisfaction Problems (PCSPs) within graph structures, which is subsequently applied to three specific optimization problems. First, the SPL decomposition improves register allocation by accurately modeling the interference graph of variables, facilitating efficient and optimal register assignments that yield marked performance enhancements across various benchmarks. Second, the general solution for PCSPs is leveraged to optimize LOSPRE, enabling effective identification and elimination of redundancies in program execution. Finally, this thesis addresses the placement of bank selection instructions, focusing on optimizing the allocation of instructions that dictate memory bank access during program execution to enhance data retrieval efficiency and reduce latency. Through extensive experimentation, the proposed algorithms exhibit significant performance improvements over existing methods, achieving optimal solutions for a diverse range of benchmark instances. In conclusion, this work establishes the SPL decomposition as a powerful instrument for tackling complex compiler optimization problems, demonstrating its effectiveness in developing efficient algorithms for register allocation, LOSPRE, and bank selection, thereby contributing to enhanced performance in modern compilers.
Faster Chaitin-like Register Allocation via Grammatical Decompositions of CFGs
OptimizationMar 2025 — ASPLOS'25 CORE A*CCF-A
Authors: X. Cai, A.K. Goharshady, S. Hitarth, C.K. Lam
It is well-known that control-flow graphs (CFGs) of structured programs are sparse. This sparsity has been previously formalized in terms of graph parameters such as treewidth and pathwidth and used to design faster parameterized algorithms for numerous compiler optimization, model checking and program analysis tasks.
In this work, we observe that the known graph sparsity parameters fail to exactly capture the kind of sparsity exhibited by CFGs. For example, while all structured CFGs have a treewidth of at most 7, not every graph with a treewidth of 7 or less is realizable as a CFG. As a result, current parameterized algorithms are solving the underlying graph problems over a more general family of graphs than the CFGs.
To address this problem, we design a new but natural concept of graph decomposition based on a grammar that precisely captures the set of graphs that can be realized as CFGs of programs. We show that our notion of decomposition enables the same type of dynamic programming algorithms that are often used in treewidth/pathwidth-based methods. As two concrete applications, using our grammatical decomposition of CFGs, we provide asymptotically more efficient algorithms for two variants of the classical problem of register allocation. Our algorithms are asymptotically faster not only in comparison with the non-parameterized solutions for these problems, but also compared to the state-of-the-art treewidth/pathwidth-based approaches in the literature. For minimum-cost register allocation over a fixed number of registers, we provide an algorithm with a runtime of O(|G| · |𝕍|5·r) where |G| is the size of the program, 𝕍 is the set of program variables and r is the number of registers. In contrast, the previous treewidth-based algorithm had a runtime of O(|G| · |𝕍|16·r). For the decision problem of spill-free register allocation, our algorithm’s runtime is O(|G| · r5·r+5) whereas the previous works had a runtime of O(|G| · r16·r).
Finally, we provide extensive experimental results on spill-free register allocation, showcasing the scalability of our approach in comparison to previous state-of-the-art methods. Most notably, our approach can handle real-world instances with up to 20 registers, whereas previous works could only scale to 8. This is a significant improvement since most ubiquitous architectures, such as the x86 family, have 16 registers. For such architectures, our approach is the first-ever exact algorithm that scales up to solve the real-world instances of spill-free register allocation.
Faster Lifetime-optimal Speculative Partial Redundancy Elimination for Goto-free Programs
OptimizationNov 2024 — SETTA'24 CCF-C
Authors: X. Cai, A.K. Goharshady
Lifetime-optimal Speculative Partial Redundancy Elimination (LOSPRE) is one of the most classical, ubiquitous and effective techniques used by compilers for redundancy elimination, i.e. avoiding unnecessary recomputations of the same expression. State-of-the-art methods for LOSPRE over structured programs are based on treewidth, i.e. they first compute a tree decomposition of the control-flow graph of the program and then perform dynamic programming on this decomposition. In this work, we consider a different decomposition approach which is called series-parallel-loop (SPL) and was recently introduced in [8]. We present an efficient linear-time LOSPRE algorithm that builds upon SPL decompositions. We then provide extensive experimental results over the Small Device C Compiler (SDCC) benchmarks, demonstrating that our algorithm outperforms the highly-optimized treewidth-based approach of SDCC.
Teaching & TA
Concurrent Programming
MT 2026–27 — Oxford
Instructor: Prof. Vincent Cheval
Principles of Programming Languages
MT 2026–27 — Oxford
Instructor: Prof. Samuel Staton
Design and Analysis of Algorithms
HT 2025–26 — Oxford
Instructor: Prof. Sandra Kiefer
Functional Programming
MT 2025–26 — Oxford
Instructor: Prof. Andrzej Murawski
Discrete Mathematical Tools for CS (Honors)
Fall 2024–25 — HKUST
Instructor: Prof. Amir Goharshady
Discrete Mathematical Tools for CS
Spring 2023–24 — HKUST
Instructor: Prof. Sunil Arya and Prof. Jiasi Shen
Introduction to Computer Networks
Spring 2021–22 — UW–Madison
Instructor: Prof. Suman Banerjee
Experience
Conferences
- CAV'26 — Lisbon, Portugal (July 26–29, 2026), presenter
- SETTA'25 — Oxford, UK (Dec 1–3, 2025), presenter & local organization team
- SETTA'24 — Hong Kong SAR (Nov 26–28, 2024), presenter
- FM'24 — Milan, Italy (Sep 9–13, 2024)
Summer School
- HUAWEI 2012 Lab Summer School — Dongguan, China (Aug. 17–21, 2026)
- Summer School on Discrete Mathematics — Prague, Czech (July 1–5, 2024)
Contact
When contacting me, please always CC my Outlook email (louiscaixuran@outlook.com).
If you’d like the full CV, click the Download CV button at the top.