Conditional Dyck-CFL Reachability Analysis for Complete and Efficient Library Summarization. - Hao Tang; Di Wang 017; Yingfei Xiong 001; Lingming Zhang 001; Xiaoyin Wang; Lu Zhang 023 (ESOP, 2017)

TiML: a functional language for practical complexity analysis with invariants. - Peng Wang 048; Di Wang 017; Adam Chlipala (Proc. ACM Program. Lang., 2017)

PMAF: an algebraic framework for static analysis of probabilistic programs. - Di Wang 017; Jan Hoffmann 002; Thomas W. Reps (PLDI, 2018)

Resource-guided program synthesis. - Tristan Knoth; Di Wang 017; Nadia Polikarpova; Jan Hoffmann 002 (PLDI, 2019)

A Denotational Semantics for Low-Level Probabilistic Programs with Nondeterminism. - Di Wang 017; Jan Hoffmann 002; Thomas W. Reps (MFPS, 2019)

Type-guided worst-case input generation. - Di Wang 017; Jan Hoffmann 002 (Proc. ACM Program. Lang., 2019)

Tail Bound Analysis for Probabilistic Programs via Central Moments. - Di Wang 017; Jan Hoffmann 002; Thomas W. Reps (CoRR, 2020)

Liquid resource types. - Tristan Knoth; Di Wang 017; Adam Reynolds; Jan Hoffmann 002; Nadia Polikarpova (Proc. ACM Program. Lang., 2020)

Raising expectations: automating expected cost analysis with types. - Di Wang 017; David M. Kahn; Jan Hoffmann 002 (Proc. ACM Program. Lang., 2020)

Central moment analysis for cost accumulators in probabilistic programs. - Di Wang 017; Jan Hoffmann 002; Thomas W. Reps (PLDI, 2021)

Sound probabilistic inference via guide types. - Di Wang 017; Jan Hoffmann 002; Thomas W. Reps (PLDI, 2021)

Expected-Cost Analysis for Probabilistic Programs and Semantics-Level Adaption of Optional Stopping Theorems. - Di Wang 017; Jan Hoffmann 002; Thomas W. Reps (CoRR, 2021)

Static Analysis of Probabilistic Programs: An Algebraic Approach - Di Wang 017 (2022)

Probabilistic Resource-Aware Session Types. - Ankush Das; Di Wang 017; Jan Hoffmann 002 (Proc. ACM Program. Lang., 2023)

Formalizing, Mechanizing, and Verifying Class-Based Refinement Types. - Ke Sun 017; Di Wang 017; Sheng Chen 008; Meng Wang 002; Dan Hao 001 (ECOOP, 2024)

Formalizing, Mechanizing, and Verifying Class-Based Refinement Types (Artifact). - Ke Sun 017; Di Wang 017; Sheng Chen 008; Meng Wang 002; Dan Hao 001 (Dagstuhl Artifacts Ser., 2024)

Semantics Lifting for Syntactic Sugar. - Zhichao Guan; Yiyuan Cao; Tailai Yu; Ziheng Wang; Di Wang 017; Zhenjiang Hu (Proc. ACM Program. Lang., 2024)

Programmable MCMC with Soundly Composed Guide Programs. - Long Pham; Di Wang 017; Feras A. Saad; Jan Hoffmann 002 (Proc. ACM Program. Lang., 2024)

Newtonian Program Analysis of Probabilistic Programs. - Di Wang 017; Thomas W. Reps (Proc. ACM Program. Lang., 2024)

Newtonian Program Analysis of Probabilistic Programs (Artifact). - Di Wang 017; Thomas W. Reps (Zenodo, 2024)

Decomposition-based Synthesis for Applying Divide-and-Conquer-like Algorithmic Paradigms. - Ruyi Ji; Yuwei Zhao; Yingfei Xiong 001; Di Wang 017; Lu Zhang 023; Zhenjiang Hu (ACM Trans. Program. Lang. Syst., 2024)

Artifact for OOPSLA'24: Semantics Lifting for Syntactic Sugar. - Zhichao Guan; Yiyuan Cao; Tailai Yu; Ziheng Wang; Di Wang 017; Zhenjiang Hu (Zenodo, 2024)

Artifact for OOPSLA'24: Semantics Lifting for Syntactic Sugar. - Zhichao Guan; Yiyuan Cao; Tailai Yu; Ziheng Wang; Di Wang 017; Zhenjiang Hu (Zenodo, 2024)

Automatic Linear Resource Bound Analysis for Rust via Prophecy Potentials. - Qihao Lian; Di Wang 017 (Proc. ACM Program. Lang., 2025)

C*: Unifying Programming and Verification in C. - Yiyuan Cao; Jiayi Zhuang; Houjin Chen; Jinkai Fan; Wenbo Xu; Zhiyi Wang; Di Wang 017; Qinxiang Cao; Yingfei Xiong 001; Haiyan Zhao 001; Zhenjiang Hu (CoRR, 2025)