Refunctionalization of abstract abstract machines: bridging the gap between abstract abstract machines and abstract definitional interpreters (functional pearl). - Guannan Wei 001; James M. Decker; Tiark Rompf (Proc. ACM Program. Lang., 2018)

Graph Neural Reasoning for 2-Quantified Boolean Formula Solvers. - Zhanfu Yang; Fei Wang 046; Ziliang Chen 001; Guannan Wei 001; Tiark Rompf (CoRR, 2019)

Precise reasoning with structured time, structured heaps, and collective operations. - Grégory M. Essertel; Guannan Wei 001; Tiark Rompf (Proc. ACM Program. Lang., 2019)

Staged abstract interpreters: fast and modular whole-program analysis via meta-programming. - Guannan Wei 001; Yuxuan Chen; Tiark Rompf (Proc. ACM Program. Lang., 2019)

BDA: practical dependence analysis for binary executables by unbiased whole-program path sampling and per-path abstract interpretation. - Zhuo Zhang 002; Wei You 001; Guanhong Tao 001; Guannan Wei 001; Yonghwi Kwon 001; Xiangyu Zhang 001 (Proc. ACM Program. Lang., 2019)

Compiling symbolic execution with staging and algebraic effects. - Guannan Wei 001; Oliver Bracevac; Shangyin Tan; Tiark Rompf (Proc. ACM Program. Lang., 2020)

LLSC: a parallel symbolic execution compiler for LLVM IR. - Guannan Wei 001; Shangyin Tan; Oliver Bracevac; Tiark Rompf (ESEC/SIGSOFT FSE, 2021)

Reachability types: tracking aliasing and separation in higher-order functional programs. - Yuyan Bao; Guannan Wei 001; Oliver Bracevac; Yuxuan Jiang 006; Qiyang He; Tiark Rompf (Proc. ACM Program. Lang., 2021)

What If We Don't Pop the Stack? The Return of 2nd-Class Values. - Anxhelo Xhebraj; Oliver Bracevac; Guannan Wei 001; Tiark Rompf (ECOOP, 2022)

What If We Don't Pop the Stack? The Return of 2nd-Class Values (Artifact). - Anxhelo Xhebraj; Oliver Bracevac; Guannan Wei 001; Tiark Rompf (Dagstuhl Artifacts Ser., 2022)

Compiling Parallel Symbolic Execution with Continuations. - Guannan Wei 001; Songlin Jia; Ruiqi Gao; Haotian Deng 001; Shangyin Tan; Oliver Bracevac; Tiark Rompf (ICSE, 2023)

Modeling Reachability Types with Logical Relations. - Yuyan Bao; Guannan Wei 001; Oliver Bracevac; Tiark Rompf (CoRR, 2023)

Graph IRs for Impure Higher-Order Languages (Technical Report). - Oliver Bracevac; Guannan Wei 001; Songlin Jia; Supun Abeysinghe; Yuxuan Jiang 006; Yuyan Bao; Tiark Rompf (CoRR, 2023)

Graph IRs for Impure Higher-Order Languages: Making Aggressive Optimizations Affordable with Precise Effect Dependencies. - Oliver Bracevac; Guannan Wei 001; Songlin Jia; Supun Abeysinghe; Yuxuan Jiang 006; Yuyan Bao; Tiark Rompf (Proc. ACM Program. Lang., 2023)

Escape with Your Self: Expressive Reachability Types with Sound and Decidable Bidirectional Type Checking. - Songlin Jia; Guannan Wei 001; Siyuan He; Yueyang Tang; Yuyan Bao; Tiark Rompf (CoRR, 2024)

Consolidating Smart Contracts with Behavioral Contracts. - Guannan Wei 001; Danning Xie; Wuqi Zhang; Yongwei Yuan; Zhuo Zhang 002 (Proc. ACM Program. Lang., 2024)

ParDiff: Practical Static Differential Analysis of Network Protocol Parsers. - Mingwei Zheng; Qingkai Shi; Xuwei Liu; Xiangzhe Xu; Le Yu; Congyu Liu; Guannan Wei 001; Xiangyu Zhang 001 (Proc. ACM Program. Lang., 2024)

Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs. - Guannan Wei 001; Oliver Bracevac; Songlin Jia; Yuyan Bao; Tiark Rompf (Proc. ACM Program. Lang., 2024)