Hanliang Zhang 张汉樑
Applied Scientist · AWS Annapurna Labs · Toronto
I work on the compiler for AWS Trainium chips at Annapurna Labs, with a focus on formal verification.
Before AWS, I was a Ph.D. student in the Bristol PL Research Group, advised by Meng Wang and Cristina David. My research was on automatic translation of programs to Rust, combining static analysis, formal methods, and large language models. Before that, I studied at Peking University, where I worked with Zhenjiang Hu on bidirectional programming.
Publications
- CGO 2027 · to appear A Barrier-Free Synchronization Algorithm for Multi-Engine AI Accelerators arXiv
- IEEE Security & Privacy 2026 PROCTOR: An Extensible C-to-Rust Translation Framework With Static-Analysis-Driven Plug-Ins
- SETTA 2025 Automated Translation of Real-World Codebases: How Far Are We?
- PLDI 2025 Scalable, Validated Code Translation of Entire Projects using Large Language Models arXiv artifact slides video
- FSE 2025 Industry Quantifying the Benefits of Code Hints for Refactoring Deprecated Java APIs arXiv
- JFP 2024 Contract Lenses: Reasoning about Bidirectional Programs via Calculation pdf Agda slides (ICFP'24) video
- arXiv 2024 Towards Translating Real-World Code with LLMs: A Study of Translating to Rust
- CAV 2023 Ownership Guided C to Rust Translation pdf code artifact slides
Service
- 2027 PAgE @ POPL · Program Committee Principles of Agentic Engineering
- 2027 ReCode @ ICSE · Program Committee Code Translation, Transformation, and Modernization
- 2026 FTfJP @ ECOOP · Program Committee Formal Techniques for Judicious Programming
- 2024 PLDI · Artifact Evaluation Committee