Research

Research Experience

  • Towards Scalable and Incremental Probabilistic Logic Programming for Program Analysis (2024-)
    • Working with Souffle and Problog.
    • Most real world program analysis are quantitative, i.e., they are not perfectly sound or complete (e.g., false alarms), or they have innately probabilistic semantics (side-channel analysis). Quantitative reasoning helps to further categorize the output of program analysis. However existing techiniques are neither scalable nor incremental.
    • Preparing for submission.
  • 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.