Heng Zhong (仲 恒)

e-mail: hzhong21@m.fudan.edu.cn

Department of Computer Science, Fudan University

Undergraduate

Research Interests

Programming languages, especially type systems; formal methods in software sngineering

Education

Research Experience

4. Meerkat: distributed semantics with causal consistency

Mentor: Prof. Jonathan Aldrich, Carnegie Mellon University

Developing Meerkat, a reactive programming language supporting live-update and unifying frontends and backends with native distributed support. Static soundness guarantee by our specially designed type system incorporating dependencies.

Implemented a concurrent interpreter in the Rust programming language and the Tokio library.

Submitted a paper [2] for ACM SPLASH Companion'24. Accepted

3. LLM-assisted software vulnerability finding

Mentor: Prof. Mayur Naik, University of Pennsylvania

Using large language models to write formal specifications and also help source-path-sink analysis, helping finding CWE vulnerability. We also constructed a high-quality dataset largest up to our best knowledege.

I am in charge of the work on vulnerability detection on JavaScript programs. In progress.

2. Zombie: A software caching and rematerialization system

Mentor: Prof. Pavel Panchekha, The University of Utah

Design and implemented a software caching system, and a purely functional language built thereon. This system allows programs to continue running (albeit slower) while using much less memory than necessary to store all of the program's heap-accessible values.

Detailed results are shown in paper [1]. The project repository itself is stored at https://github.com/MarisaKirisame/zombie and https://github.com/MarisaKirisame/TVirus

1. Design and Optimization of Graph Isomorphism Algorithms

Advisor: Prof. Haibin Kan, Fudan University

• Significantly optimized the VF algorithm using the method of canonical labeling of graphs, reducing the candidate vertices in the matching procedure using WL refinement.
• Result: Non-isomorphic cases can be detected in O(n^2) time during preprocessing with only probability exp(-cn log n/log log n) of failure. Moreover, in the failure and isomorphic cases, the average running time in experiment has decreased by more than a half.

Papers

[1] Marisa Kirisame, Sihao Chen, Heng Zhong, Tiezhi Wang, Pavel Panchekha. Uncomputation. Not yet submitted and some minor parts remain to be fixed. Newest version available at https://github.com/MarisaKirisame/zombie_paper

[2] Heng Zhong* and Anrui Liu*. 2024. Meerkat: Distributed Reactive Live Semantics with Causal Consistency. In Companion Proceedings of the 2024 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH Companion '24). Association for Computing Machinery, New York, NY, USA, 52–53. https://doi.org/10.1145/3689491.3691822. *Both authors contributed equally to the research.

Skills

Programming: C (8 years experience); Standard ML, OCaml, Rust, Verilog/SystemVerilog (Experienced); Modern C++, Haskell (Familiar); Coq (Learning)

Language: English (Highly Proficient, GRE 331), Chinese (Native), Japanese (Learning)

Recent work

Important Coursework

• Set theory & graph theory (honor)
• Algebraic structures & mathematical logic (honor)
• Functional programming
• Theory of computation
• Cryptography
• Database systems
• Computer organization & architecture (honor)
• Operating systems
• Principles of programming languages
• Compilers (honor)