Curriculum Vitae
Aosen Xiong
Ph.D. candidate, Electrical and Computer Engineering, University of Waterloo
aosen.xiong@uwaterloo.ca |
ece.uwaterloo.ca/~a4xiong |
github.com/aosen-xiong
Programming languages and formal verification researcher working on type systems, mechanized metatheory, static analysis, and verified developer tooling. My work combines Lean/Rocq formalization with practical language tools for Java and Dafny.
Technical Skills
Programming: Java, C++, Python, F#, Rust
Verification and theorem proving: Lean 4, Rocq, Dafny, Boogie, SMT solving
Education
Expected graduation: Fall 2027
Advisor: Werner Dietl
Supported by the International Doctoral Student Award and Graduate Research Studentship
Supported by the Entrepreneurial PhD Fellowship
Industry Experience
With Dr. Rustan Leino
- Designed a region type system for Dafny to improve verification performance, controlled aliasing, and abstraction boundaries.
- Implemented an executable verifier prototype for a minimal language by translating region-typed programs to Boogie verification conditions.
- Developed a Dafny proof of key type-safety properties for the type-system design.
With Jenny Xiang
- Integrated an immutability type checker into internal AWS Java code to evaluate practical annotation requirements and compatibility constraints.
- Extended Dafny-to-Java compiler support to preserve immutability specifications through generated Java annotations.
- Identified a Dafny-to-Java compiler design bug exposed by immutability annotation translation.
- Evaluated the translation on more than 4,000 lines of internal code with 67 immutability annotations.
Selected Research Projects
PICO / Java immutability
- Designed PICO, a pluggable type system for transitive abstract immutability in Java with receiver-dependent mutability and class-level mutability polymorphism.
- Implemented PICO in the Checker Framework and mechanized its core metatheory in Rocq, proving type soundness and immutability properties.
- Evaluated PICO on Java Collections Framework code in OpenJDK 17 and other benchmarks, covering approximately 26,000 non-comment lines of Java code.
GAIT / Generic Abstract Immutability Types
- Designed a generic immutability calculus combining receiver-dependent qualifiers, class-level qualifier polymorphism, and requalified type variables.
- Mechanized static semantics, runtime semantics, and type-safety in Lean 4, resolving generic substitution, recursive viewpoint adaptation, and object-relative runtime type arguments.
- Status: draft submitted to IWACO 2026.
Reusable Qualifier Framework in Lean 4
- Built reusable Lean 4 infrastructure for qualifier lattices, static typing, runtime semantics, runtime typing, progress, preservation, and soundness packaging.
- Instantiated the framework with multiple checkers, including Nullness, Readonly, Tainting, Confidentiality, Universe, and PICO.
Open Source
Checker Framework / type systems, static analysis
Active contributor to the Checker Framework and Checker Framework Inference, including improvements around Nullness and Initialization checking, soundness bug fixes, and pull request reviews.
Publications
- Aosen Xiong, Yudi Bai, Haifeng Shi, Lian Sun, Mier Ta, and Werner Dietl. Transitive, Abstract, and Class Polymorphic Immutability. To appear at OOPSLA 2026.
- Aosen Xiong and Werner Dietl. Generic Abstract Immutability Types. Submitted to IWACO 2026.
Teaching
Teaching Assistant: SE 465 Software Testing and Quality Assurance (2025); ECE 653 Testing, Quality Assurance, and Maintenance (2024); ECE 650 Methods and Tools for Software Engineering (2024); SE 464 Software Design and Architectures (2023).
Awards and Honors
CAV VMW Scholarship (2024); Oregon Programming Languages Summer School Fellowship (2024); PLMW Scholarship - PLDI SIGPLAN (2023).
Academic Service
TACAS Artifact Evaluation Committee (2025, 2026); SPIN Artifact Evaluation Committee (2025); ECOOP Artifact Evaluation Committee (2025); CAV Student Volunteer (2024); ECE Graduate Student Mentor, University of Waterloo (2023-current).