About Me

I am a master student at Xi'an Jiaotong University (XJTU), advised by Prof. Peng Zhang.

My research interests span vastly across computer sciences: majorly focusing on formal methods, computer systems, and software engineering. Currently I'm working on formal verification and automated reasoning: satisfiability modulo theories (SMT) solvers and binary decision diagrams (BDD). Previous research experiences include network configuration repair (ACR), network simulation & verification, and AI.

In extracurricular life, I love tennis, photography, video editing, sketching, graphics design, web development, open source development, etc.

View my CV

Research Interests

  • Formal Methods: SMT Solvers, BDDs, Automata, Model Checking
  • Networked / Operating Systems: Network Simulation System, Automatic Configuration Repair
  • Software Engineering: Automatic Program Repair (APR), Formal Software Verification

Education

  • Master Student, Advanced Networked System Group, Xi'an Jiaotong University
    Advisor: Prof. Peng Zhang
    -
  • B.Eng. in Honor Science Program (Computer Science), Xi'an Jiaotong University
    GPA: 3.95/4.3, Average Score 91.6, Rank 4/37
    Thesis: Design and Implementation of Scalable Network Emulation System
    -
  • Visiting International Student Program (VISP), Computer Science Thematic Track, University of Wisconsin-Madison
    GPA: 4.00/4.0, Average Score A
    -
  • Honor Youth Program, Xi'an Jiaotong University & Suzhou High School - SIP
    -

Experiences

  • Internship, ByteDance
    Network Development
    -

Publications

Selected Talks

  • Astragalus: Automatic Configuration Repair for Production Networks

    SIGOPS ATC 2026, Hong Kong SAR (scheduled)

    Abstract

    Network configurations are prone to errors, which can lead to catastrophic service outages. A tool that can achieve automatic configuration repair (ACR) is highly desired by operators. Existing tools for ACR follow a semantics-driven approach: they model network semantics as a set of SMT constraints, and solve them for a location or fix of the error. Due to the complex semantics of networks, constructing and solving these constraints can be prohibitively expensive, making these tools neither general nor scalable. Inspired by automatic program repair (APR), we explore another direction, i.e., a syntax-driven approach, which generates and validates syntactically-valid candidate updates without modeling program semantics, often drawing on existing code in the same repository. Following this direction, we propose Astragalus, a syntax-driven method for ACR. It uses multiple iterations of a “localize-fix-validate” pipeline to search for repairs, and proves quite effective on configurations of our production network. Specifically, we show that Astragalus can repair every incident in multiple sizes of a synthesized network, and 97.5% of the incidents on a real network, both with 15 types of errors injected, within an average time of 6.93 seconds. It has also provided valid repair suggestions in under 6 minutes for 7 recent network incidents or undesired changes, in a real production network with O(1,000)–O(10,000) devices.

  • Network Verification and BDDs

    Invited talk, University of Wisconsin–Madison, Madison, USA

    Abstract

    Network outages caused by configuration errors and data-plane bugs have become routine headlines, and formal verification is the natural response. Tools such as APKeep and Symbolic Router Execution (SRE) model a network as a graph of standardized packet (or route) filters and transformers, and symbolically simulate packet forwarding, reducing an intractable header space to a small number of equivalence classes represented as BDDs. With the rapid expansion of data centers, this approach is facing scalability issues. One observation makes such representations far cheaper: the variables in a network verification problem are organized into fields, and the logic over each field is highly repetitive and reusable across devices. Network Decision Diagrams (NSDI ’25) exploit this by branching one field at a time and representing each edge as a shareable BDD, yielding large speedups and memory savings for APKeep and improved scalability for SRE.

    I will then discuss two limits of NDDs: quantitative properties requiring multi-terminal representations, and the difficulty of choosing a field granularity for link status. Both may be addressed by Generalized CFLOBDDs, introduced by Meghana Sistla, which use a custom grammar to describe variable organization and permit a loose recursive hierarchy with external decision diagrams at the leaves. Building on that idea, I have been formalizing the structure: a Rust implementation, a canonicity proof, structural optimizations, and an evaluation on network verification and quantum simulation. I will present the canonicity argument and these early results, and close with some open questions about the future of NDDs and CFLOBDDs.

  • Relia: Accelerating the Analysis of Cloud Access Control Policies

    ASE 2025, Seoul, South Korea

    Abstract

    With the diversification of cloud services, cloud providers offer flexible access control by letting users apply fine-grained cloud access control policies to secure their cloud resources. However, flexibility comes with the cost that configuring cloud access control policies is error-prone. Therefore, cloud providers have developed SMT-based tools to formally analyze the user-defined policies. Unfortunately, we find these analyzers slow, due to the complex regular expression matching conditions in policies. To this end, this paper introduces Relia, a general method to speed up the analysis of cloud access control policies. The key idea of Relia is to pre-compute a set of String Equivalence Classes (SECs) based on the regular expressions in a policy, assign a unique integer to each SEC, and rewrite the regular constraints into equivalent integer constraints, which are easier to solve. We implement Relia as a transparent layer between our in-house access analyzer and off-the-shelf SMT solvers. Based on real policies from a large public cloud provider, we show that: when enabling Relia, our in-house portfolio solver (consisting of Z3, Cvc4, and Cvc5) can speed up the analysis process for nearly 95% of all cases, with an average speedup of 8.21×.

Awards

  • Outstanding Graduate Leader of Xi'an Jiaotong University
  • Bronze Award, 2021 International Collegial Programming Contest
    Asia Jinan Regional Contest (Ranked 108th / 726)
  • First Prize, 12th “Lanqiao” Cup National Software and Information Technology Contest
    Track of Java Software Development (Ranked 6th Nationally)

Skills

Computer Skills

Languages: Proficiency in C, advanced Rust and C++, TypeScript, JavaScript, Java, Python and Go

Formal Methods: Z3 / cvc5 for SMT solving, BDD/decision-diagram libraries, LEAN and formal proof assistants

Systems and Development: System programming, proficient GNU/Linux skills (GCC / GDB / Shell), Linux kernel hacking and eBPF, embedded systems, fullstack web development

Languages

English: TOEFL iBT 5.5/6.0 (Reading 6.0, Listening 6.0, Writing 5.5, Speaking 5.0)