Guannan Wei🔗

• Email:
 guannan.wei@inria.fr
 guannan.wei@tufts.edu
• Google Scholar | DBLP | Github
• Instagram | Gallery | Twitter

Recent services:
• PC: TFPIE 2025, PLDI 2025, OOPSLA 2025

• Curriculum Vitae
• Research Statement
• Teaching Statement
• Diversity Statement

I am a postdoctoral researcher in the ANTIQUE team at INRIA and École Normale Supérieure (Paris), working with Caterina Urban. I am also a visiting assistant professor at Tufts University.

Previously, I was a postdoctoral researcher at Purdue University, and I obtained my Ph.D. in Computer Science from Purdue University, advised by Tiark Rompf. I received M.S. degree in Computer Science from the University of Utah, advised by Matt Might. I was an intern at SambaNova Systems, Galois, and Baidu. I occasionally take notes of what I read, collect elegant programs, or post random thoughts in my Blog.

I will join CS@Tufts as an Assistant Professor in Fall 2025. If you are interested in working with me in programming languages, formal methods, or software engineering, feel free to reach out!

Research🔗

I study the scientific and engineering aspects of programming, driven by a fascination with how it allows people creating abstractions and communicating ideas. My research aims to develop novel notions and tools that empower people to build correct, safe, and efficient software.

More specifically, I am interested in type systems, program analysis/verification/testing, compilers/interpreters, metaprogramming, as well as their applications.

• High-performance program analyzers via compilation/metaprogramming.

  We have developed compilation [ICSE ’23, PEPM ’22, FSE ’21, OOPSLA ’20, OOPSLA ’19], derivation [ICFP ’18], and transformation techniques [OOPSLA ’19] to build correct-by-construction, performant, and flexible program analyzers, enabling to use higher-level abstractions yet without compromising performance or correctness.

  Our parallel symbolic-execution compiler GenSym [ICSE ’23] demonstrates efficient (4x vs KLEE, single-thread) execution by compiling to continuation-passing style via the 1st Futamura projection.

• Type systems tracking aliases, separation, and effects for imperative higher-order languages.

  We have designed reachability types with a flow-sensitive effect system [OOPSLA ’21], offering programmers Rust-style reasoning principles in more expressive and flexible higher-order languages. Reachability types have been used to guide optimizatoins in graph-based compiler IRs [OOPSLA ’23] and extended with \texttt{F}_{<:}-style type-and-reachability polymorphism [POPL ’24]. We have also designed a type system to track storage modes, enabling flexible and efficient memory allocation on the stack [ECOOP ’22].

  We are implementing a prototype programming language Diamond with \texttt{F}_{<:}-style precise and polymorphic reachability types.

Publications🔗

Conference/Workshop Papers

• Consolidating Smart Contracts with Behavioral Contracts
  Guannan Wei, Danning Xie, Wuqi Zhang, Yongwei Yuan, Zhuo Zhang* (* corresponding author)
  Proceedings of the ACM on Programming Languages, Volume 8 (PLDI 2024). Copenhagen, Denmark
  [pdf] [acm dl] [artifact]

• ParDiff: Practical Static Differential Analysis of Network Protocol Parsers
  Mingwei Zheng, Qingkai Shi, Xuwei Liu, Xiangzhe Xu, Le Yu, Congyu Liu, Guannan Wei, Xiangyu Zhang
  Proceedings of the ACM on Programming Languages, Volume 8 (OOPSLA 2024). Pasadena, CA, USA
  [pdf] [acm dl] [artifact]

• Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs
  Guannan Wei, Oliver Bračevac, Songlin Jia, Yuyan Bao, Tiark Rompf
  Proceedings of the ACM on Programming Languages, Volume 8 (POPL 2024). London, United Kingdom
  [pdf] [acm dl] [arxiv] [artifact]

• Graph IRs for Impure Higher-Order Languages – Making Aggressive Optimizations Affordable with Precise Effect Dependencies
  Oliver Bračevac, Guannan Wei, Songlin Jia, Supun Abeysinghe, Yuxuan Jiang, Yuyan Bao, Tiark Rompf
  Proceedings of the ACM on Programming Languages, Volume 7 (OOPSLA 2023). Cascais, Portugal
  [pdf] [acm dl]

• Compiling Parallel Symbolic Execution with Continuations
  Guannan Wei, Songlin Jia, Ruiqi Gao, Haotian Deng, Shangyin Tan, Oliver Bračevac, Tiark Rompf
  The 45th International Conference on Software Engineering (ICSE 2023)
  [pdf] [ieee] [artifact]

• What If We Don’t Pop the Stack? The Return of Second-Class Values
  Anxhelo Xhebraj, Oliver Bračevac, Guannan Wei, Tiark Rompf
  Proceedings of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Berlin, Germany
  [pdf] [dagstuhl] [artifact]

• Towards Partially Evaluating Symbolic Interpreters for All
  Shangyin Tan, Guannan Wei, Tiark Rompf
  ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM), co-located with POPL 2022. Philadelphia, PA, USA
  [pdf] [bib]

• Reachability Types: Tracking Aliasing and Separation in Higher-Order Functional Programs
  Yuyan Bao, Guannan Wei, Oliver Bračevac, Yuxuan Jiang, Qiyang He, Tiark Rompf
  Proceedings of the ACM on Programming Languages, Volume 5 (OOPSLA 2021). Online/Chicago, IL, USA
  [pdf] [acm dl] [artifact]

• LLSC: A Parallel Symbolic Execution Compiler for LLVM IR (Tool Demonstration)
  Guannan Wei, Shangyin Tan, Oliver Bračevac, Tiark Rompf
  Proceedings of the 29th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE 2021)
  [pdf] [acm dl] [demo]

• Compiling Symbolic Execution with Staging and Algebraic Effects
  Guannan Wei, Oliver Bračevac, Shangyin Tan, Tiark Rompf
  Proceedings of the ACM on Programming Languages, Volume 4 (OOPSLA 2020). Online
  [pdf] [acm dl] [artifact]

• Staged Abstract Interpreters: Fast and Modular Whole-Program Analysis via Meta-Programming
  Guannan Wei, Yuxuan Chen, Tiark Rompf
  Proceedings of the ACM on Programming Languages, Volume 3 (OOPSLA 2019). Athens, Greece
  [pdf] [acm dl] [artifact]

• Precise Reasoning with Structured Time, Structured Heaps, and Collective Operations
  Grégory Essertel, Guannan Wei, Tiark Rompf
  Proceedings of the ACM on Programming Languages, Volume 3 (OOPSLA 2019). Athens, Greece
  [pdf] [acm dl] [artifact]

• BDA: Practical Dependence Analysis for Binary Executables by Unbiased Whole-program Path Sampling and Per-path Abstract Interpretation
  Zhuo Zhang, Wei You, Guanhong Tao, Guannan Wei, Yonghwi Kwon, Xiangyu Zhang
  Proceedings of the ACM on Programming Languages, Volume 3 (OOPSLA 2019). Athens, Greece
  [pdf] [acm dl] [artifact]

• Towards Verified Binary Raising
  Joe Hendrix, Guannan Wei, Simon Winwood
  Workshop on Instruction Set Architecture Specification, co-located with ITP 2019. Portland, OR, USA
  [pdf] [bib]

• Graph Neural Reasoning for 2-Quantified Boolean Formula Solvers
  Zhanfu Yang, Fei Wang, Ziliang Chen, Guannan Wei, Tiark Rompf
  Workshop on Learning and Reasoning with Graph-Structured Representations, co-located with ICML 2019. Long Beach, CA, USA
  [pdf] [bib]

• Refunctionalization of Abstract Abstract Machines (Functional Pearl)
  Guannan Wei, James M. Decker, Tiark Rompf
  Proceedings of the ACM on Programming Languages, Volume 2 (ICFP 2018). St. Louis, MO, USA
  [pdf] [acm dl] [artifact]

Dissertation

• Metaprogramming Program Analyzers
  Guannan Wei
  PhD Dissertation. Purdue University. 2023
  [pdf]

Talks/Posters🔗

• Metaprogramming Program Analyzers
  ANTIQUE Seminar. INRIA/ENS-PSL Paris. Oct, 2024 [slides]
  

• Consolidating Smart Contracts with Behavioral Contracts
  PLDI 2024. Copenhagen, Denmark. June, 2024 [slides]
  

• Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs
  POPL 2024. London, UK. January, 2024 [slides]
  Midwest Programming Languages Summit (MWPLS). Ann Arbor, MI. Oct, 2023 [poster]
  

• Compiling and Controlling Symbolic Execution
  Northeastern University Programming Languages Seminar. Boston, MA. Dec 2023 [slides]
  Midwest Programming Languages Summit (MWPLS). Ann Arbor, MI. Oct 2023 [slides]
  Purdue PL Seminar. West Lafayette, IN. Dec, 2022 [slides]
  

• Compiling Parallel Symbolic Execution with Continuations
  ICSE 2023. Remote. May, 2023 [slides]
  

• Reachability Types: Tracking Aliasing and Separation in Higher-Order Functional Programs
  OOPSLA 2021. Chicago, IL. Oct, 2021 [poster]
  

• LLSC: A Parallel Symbolic Execution Compiler for LLVM IR
  ESEC/FSE 2021. Online. Aug, 2021 [slides]
  

• Compiling Symbolic Execution with Staging and Algebraic Effects
  OOPSLA 2020. Online. Nov, 2020 [slides]
  

• Metaprogramming for Program Analyzers
  PurPL Retreat. Online. Aug, 2020 [slides]
  

• Staged Abstract Interpreters
  OOPSLA 2019. Athens, Greece. Oct, 2019 [slides]
  

• Refunctionalization of Abstract Abstract Machines (Functional Pearl)
  ICFP 2018. St. Louis, MO. Sept, 2018 [slides][poster]
  

• Precise Reasoning with Structured Heaps and Collective Operations à la Map/Reduce
  Purdue PL Seminar. West Lafayette, IN. January 26, 2018 [slides]
  Midwest Programming Languages Summit (MWPLS). Bloomington, IN. Dec, 2017 [slides]
  Huawei Research Summit. Urbana-Champaign, IL. Mar, 2018 [slides]
  

Mentoring🔗

Undergraduate

• Alex Bai, Tufts University, Fall 2024 -

• Mikail Khan, Purdue University, Fall 2022 - Spring 2024 (Now PhD student at CMU)

• Shangyin Tan, Purdue University, Summer 2020 - Fall 2021 (Now PhD student at UC Berkeley)

• Yuxuan Chen, Purdue University, Fall 2018 (Now Software Engineer at Meta)

Teaching🔗

• Co-instructor, CS352 Compilers: Principles and Practice (undergraduate), Purdue University, Spring 2024

• Lead Teaching Assistant, CS352 Compilers: Principles and Practice (undergraduate), Purdue University, Spring 2020
  [testimonials]

    “Guannan you are a real homie, thanks for carrying the course and helping out all the students who were lost as hell – please know that your help in this class is probably what got everyone through it, you are a blessed human being thanks for your existence :)”

    “Guannan was patient and very helpful with the projects. I’m really glad he was my TA because he helped a lot along the way.”

    “Guannan is a god on Piazza.”

    “Guannan is a great TA and is very talented. He was great at answering questions during the lab session and helping students debug their code, especially since most of us were using a language we had never used before. He was also very active on Piazza, helping me and other students whenever we had questions about the projects or lecture.”

• Teaching Assistant, CS502 Compilers: Principles and Practice (graduate), Purdue University, Fall 2019

• Lab Instructor, CS252 System Programming (undergraduate), Purdue University, Fall 2017, Spring 2018

Services🔗

• Program Committee Member: TFPIE 2025, PLDI 2025, OOPSLA 2025, SETTA 2024 (Distinguished Reviewer Award), ICCQ 2024, ICCQ 2023, VMIL 2021, EuroSys Shadow 2021

• Reviwer: TOSEM 2024, ICFP 2022, ISSTA 2021, ICLR 2019

• Artifact Evaluation Committee Member: ISSTA 2024, OOPSLA 2024, POPL 2024, ICFP 2023, PLDI 2023, POPL 2023, PLDI 2022, PLDI 2021, ICFP 2021, ISSTA 2021, OOPSLA 2020, ICFP 2020, CAV 2020, ICFP 2019

• Student Volunteer: POPL 2023, ICFP 2019, MWPLS & PurPL Fest 2019

Code & Open Source Contribution🔗

• GenSym: a compiler for parallel symbolic-execution of LLVM IR

• Diamond language: a prototype language with the polymorphic reachability type system

• Mechanizations of reachability types in Coq

• lms-clean: the Lightweight Modular Staging framework

• Voluntary translator, Software Foundations (Chinese edition)

Quotes🔗