Research

Research Experience

  • Scalable and Incremental Probabilistic Inference for Program Analysis (2024-)
    • Scale and incrementalize probabilistic inference via specialization and independence reasoning for uncertain program analyses, including side-channel analysis, unsound/incomplete analyses, and probabilistic disassembly.
    • Incremental Inference for Probabilistic Datalog has been accepted to CAV 2026 and is to appear; one related manuscript is in preparation.
    • Built with Souffle and ProbLog; mentoring undergraduate Jiahao Xia.
  • Verified Validation for Polyhedral Scheduling (2022-2024)
    • Accepted to TASE'24 with slides.
    • Mechanize a verified validator for affine scheduling in Coq. Its algorithm checks Bernstein's condition within polyhedral model.
    • Instantiated with semantic model of CompCert.
    • Adapted to validate Pluto compiler's core scheduling algorithm.
    • Open source at this repository.
  • Verified Optimization in the Promising Semantics (2021-2022)
    • With the verification framework, I adapt CompCert's verified Kildall algorithm and machanize an optimization pass (Common Subexpression Elimination, CSE) in the Promising Semantics.