{ /》ヽ
ヽ / 《¨｀ﾒ- ‐─、-‐──､_
_ - ──‐-､─‐｀／ /´｀ヽ ,_イ´ ／ /7‐-､
／ l ／ ハ ／ /´ / l l l
＿ ＞' ／´ | 八 /／ リ、 |ヽ
__ - 二￣ ／ / 八 ∨／/ ／|/∨l ﾍ へ
, - ／l ∧ ＼ ゞ /|/ 十ナﾒ ヽ ハ
, ´ ／ ＞ へ＿ ＞- ´ ／／l ./＼ ,へ/ , ｨｺｭ､ ヽ| | N| ﾘ
／ /／ , ´ ／／ / l/ | ｛ (ﾉｌ| 弋!ﾘ i/∨」| }
/ ／l ／ /) ,､. /／/ / ! l ヽ__ ｀ ´ ゝ､!| / ｌ /
! .／ ／ /.ﾉ ./ ﾉ/ ) / / / l l | lｿﾉ !/／l∧
／/ ／/ （ l.l´/ / / /＿｛ ｛ ! ハ l l＼ ､ / / ∧ .ﾉ ヽ
/ /／ / ハ l !/ l／ ,-‐'ハ ＼ !' / 丶 ヽ_ヽ 人 ＼ , ,､,､
! .// ｛. ノ. l __ ／／ ＼＼_ﾍ ! ,t=ｪｪx_ ＼ ／| ＼ ＼ ／ﾉ/ﾉl | ,
l/ ',. |/::::| /／ ／√ ｀ー｀ヽ / ⊂:⊃ ヾ __.lゝィ１´l ! |＼ ｀ｰ─ ∧/7二 .ﾅ／ﾉﾆ｀ヽ
. ｛ l|::::/ / ／ /(○）|:＼ ﾐヽ ∨| ＿,-‐!─ ､八 ＼_／/ |//:::::￣／
＼ / V /／ 〔 |:::::::〉 丶￣＼_ / ＿く＼＿ ∧ ヽ、 / ハ:::::::::::l
〈 l / /＿ ／::::/ /￣ `ー､＼／ ,ｲ ＼l:::| l ｀ー' l !::::::::l
／ _∨＿ ヽ/ / ／::::::::::/ ／／´｀ヽ ＼_／ , -‐､ヽ l | ￣ /
/ 〔 ⊂⊃〕 /. /:::::::::::::/ / / ｀ヽ ０２ ノ ＼. l /⊃｀‐- /
. / /. ｀ｰt- | ///::::::::::::/ l l: : : : : : : : : . .} l. . . : : : : }::| ＼＼ ヽ
/ / .| | ./､/:::::::::::::/ l 八: : : : : : : : ＞' ｀＜: : :/:::i / ／
. / ｛ | l/::::::::::::::::::/ l ｀ー─ ´＼ |￣|:::::::l / /
/ ﾊ/／ | l::::::::::::::::::/＼ l ＼ l ｌ:::::::l /! /
. { / l / ｌ l:::::::::::::::/l ＼ ＼ ' （([]) ）, ＼. / 「〕::::l /:::ｌ /
＼ / l .l ∧!:::::::::::/ !∧ ＼/ ｀ー-‐' ＼/ `ｌ:::::l /:::::::l ｿ
l ｌ i |::ﾍ:::::::::∧ l ∨＼|: ＼ ＿ ∨ V:::!/::::::::/ /
l ﾄ､ l l::::ﾍ:::::/ ＼ ! ＼ ￣ ﾍ. Vl::::::::::l /
l l | l::::∧/ ＼ ,ﾘハリ/ヽ∠ _ ' , 〉、／ /
ﾍ l | l:/ ./ ｀ヽ ＼ ＿ ＼ 〉､__/
＼ ＼＿ノ |/´ ｀ヽ ' , ﾍ
ll ∧ ' , ｌ.ﾍ
ｌ| ' , ', .l ﾍ
|l '., i l ﾍ
l , l l ﾍ
l ＿ , l l ﾍ
l ￣二丶', | l ハ
| ｀ヽ. | ｌ ∧
l ＼ ノ ∧
l＿＿＿＿＿＿ ＿. ＼ ∧
〔＿:::::::::::::::::::::::::::───::::::::::＼ ∧Ph.D. student in Computer Science & Engineering at UC Santa Cruz
Zheyuan Chen is a Ph.D. student in Computer Science & Engineering at UC Santa Cruz working on GPU semantics, formal verification, portable GPU kernels, and ML systems.
I’m Zheyuan Chen, a Ph.D. student in Computer Science & Engineering at the University of California, Santa Cruz. I’m advised by Prof. Tyler Sorensen and work on GPU semantics, formal methods, compilers, and portable ML kernels.
I am particularly interested in GPU semantics and highly efficient portable kernel design. I believe that the lack of precise, formal semantics in current GPU programming models, especially around subgroup execution, synchronization, and memory consistency, limits our ability to reason about correctness and performance portability. My research aims to develop formal foundations and practical tools for rigorous reasoning about GPU behavior, and to leverage these insights to design portable kernels that achieve both correctness and high performance across heterogeneous architectures.
One way to summarize the kind of systems work I like is:
struct Research {
focus: [GpuSemantics, FormalVerification, PortableKernels],
}
impl Research {
fn optimize(&self) -> Goal {
semantics::model(SubgroupBehavior)
.verify_with(FormalMethod)
.compile_to(PortableGpuKernel)
}
}
const GOAL: &str = "Correct and fast kernels across architectures";The quickest way to navigate this site is through my publications, CV, and public code on GitHub.
Updates
View allResearch
View allLlamaWeb brings memory-efficient, performance-portable, multi-precision LLM inference to the browser with a WebGPU backend for llama.cpp, reducing memory use and improving decode throughput across diverse devices.
SIMT-Step provides a formal and flexible operational semantics for GPU subgroup execution, using dynamic basic blocks and TLA+ validation to reason about converged, synchronous, and independent behaviors across devices.
BetterTogether enables fine-grained software pipelining on heterogeneous edge SoCs using a profile-guided performance model that captures intra-application interference across CPUs and GPUs.
sqlelf models ELF objects as relational databases, enabling expressive SQL queries, aggregation, and cross-object analysis for more accessible and efficient ELF exploration.
Teaching