Skip to content
View Ao-senXiong's full-sized avatar
6 followers · 68 following
  • University of Waterloo
  • Waterloo, ON, Canada
  • 06:04 (UTC -12:00)

Achievements

Achievement: Pair Extraordinairex3Achievement: Pull Sharkx3Achievement: YOLOAchievement: Quickdraw

Achievements

Achievement: Pair Extraordinairex3Achievement: Pull Sharkx3Achievement: YOLOAchievement: Quickdraw

Organizations

@eisop @eisopux

Block or report Ao-senXiong

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Please don't include any personal information such as legal names or email addresses. Maximum 100 characters, markdown supported. This note will be visible to only you.
Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse
Ao-senXiong/README.md

Aosen Xiong

EIT 4167, Ring Rd, Waterloo, ON N2L 3G1

Education

Ph.D. in Electrical and Computer Engineering
University of Waterloo (2022 – ?)

B.Eng. in Engineering
Chongqing University (2017 – 2021)

Research Interests

  • Pluggable type systems and optional type checking
  • Type inference for reducing annotation burdens
  • Lightweight formal methods for program correctness

Professional Experience

Applied Scientist Intern
Amazon, Automated Reasoning Group (2024)

  • Applied an immutability type checker to AWS internal codebases.
  • Translating Dafny to Java with Checker Framework annotations.

Graduate Research Assistant
University of Waterloo (2023 – Present)

  • Contributed to an immutability type checker and inference tools for Java.
  • Worked on the Checker Framework, fixing false negatives and adding new features for Nullness and Initialization checkers.
  • Developed a VSCode extension using LSP to detect potential errors and improve IDE support for pluggable type systems.

Selected Projects

Checker Framework Contributions

  • Improved nullness and initialization checkers to enhance static analysis tools for Java developers.

PICO: Practical Immutability for Classes and Objects

  • Built an optional immutability type checker for Java and implemented type inference to reduce annotation overhead.

Joos Compiler

  • Created a Java subset compiler, implementing lexer, parser, semantic analysis, and code generation.

Boolean Satisfiability Solver

  • Developed a SAT solver using the DPLL algorithm and Tseitin transformation to handle formulae in conjunctive normal form.

Awards and Honors

  • CAV VMW Scholarship, 2024
  • Oregon Programming Languages Summer School Fellowship, 2024
  • PLMW Scholarship (PLDI), 2023

Publications and Presentations

Presentations

  • Talk: Practical Class and Object Immutability, University of Toronto and University of Waterloo Programming Language Meetup (Apr. 2024).
  • Poster: Pluggable Properties for Program Correctness, Cybersecurity and Privacy Institute Annual Conference (Oct. 2024).

Teaching Experience

University of Waterloo

  • Testing, Quality Assurance, and Maintenance (ECE 653) – Teaching Assistant, 2024
  • Methods and Tools for Software Engineering (ECE 650) – Teaching Assistant, 2024
  • Software Design and Architectures (SE 464) – Teaching Assistant, 2023 Fall

Academic Service

  • Artifact Evaluation: TACAS 2025, SPIN 2025

Contact

Last updated: November 2024

Pinned Loading

  1. eisop/checker-framework eisop/checker-framework Public

    Forked from typetools/checker-framework

    Pluggable type-checking for Java

    Java 19 19

  2. opprop/checker-framework-inference opprop/checker-framework-inference Public

    Forked from typetools/checker-framework-inference

    Inference of pluggable types for Java

    Java 6 13

  3. eisopux/checker-framework-vscode eisopux/checker-framework-vscode Public

    Checker Framework for VS Code

    TypeScript 4 8

  4. checker-framework-languageserver checker-framework-languageserver Public

    Forked from eisopux/checker-framework-languageserver

    Checker Framework Language Server

    Java