Research

Research Experience

  • Agentic Compiler Testing for ML Compilers (2026.5-2026.8)
    • At Amazon Annapurna Labs, developed agentic compiler testing for semantic miscompilations in ML compilers.
    • Found 120+ bugs in TileLang (50+ fixed) and about 10 bugs in Triton.
  • Scalable and Incremental Probabilistic Logic Inference (2025-Present)
    • Develop scalable and incremental probabilistic logic inference with Soufflé and ProbLog, with applications to program analysis.
    • Incremental Inference for Probabilistic Datalog, CAV 2026.
    • PSoufflé: Scaling Exact Probabilistic Logic Inference for Program Analysis, FMCAD 2026.
  • Verified Polyhedral Compilation (2022-Present)
    • Develop PolCert, a polyhedral compiler verified in Rocq (Coq), from source loop IR to optimized loop IR.
    • Combine verified loop extraction and code generation with validation of Pluto transformations, including affine scheduling, index-set splitting, tiling, and parallelization.
    • Initial work on verified affine scheduling appeared at TASE 2024.
  • Verified Optimization under Promising Semantics (2021-2022)
    • Verified common-subexpression elimination in Coq under promising semantics.
    • Released as part of a PLDI 2022 artifact.