Research
Research Experience
-
Verified Validation for Polyhedral Scheduling
- Accepted to TASE'24.
- 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
- With the verification framework, I adapt CompCert's verified Kildall algorithm and machanize an optimization pass (Common Subexpression Elimination, CSE) in the Promising Semantics.