Hongfei Fu

Contact:

Email: ("hongfeifu" + "1984") at gmail.com

Research Interest

My primary interest includes programming language and formal verification in a broad sense.

PhD Thesis

Verifying Probabilistic Systems: New Algorithms and Complexity Results [link], RWTH Aachen, Germany

Teaching

Python Programming (Fall 2024 -- 2025)
Foundations of Programming Languages (Spring 2018 -- 2021)
Discrete Mathematics (Fall 2018 -- 2023)
Program Analysis and Verification (Spring 2020)
Model Checking (Spring 2022 -- 2026)

Publications

Book Chapter

Termination Analysis of Probabilistic Programs with Martingales [Link]
Foundations of Probabilistic Programming, Cambridge University Press, 2020
(with Krishnendu Chatterjee and Petr Novotny)

Probabilistic Programming

Probabilistic Floating-Point Round-Off Analysis via Concentration Inequalities
ACM SIGPLAN International Conference on Object-Oriented Programming Systems, Languages, and Applications
OOPSLA 2026, to appear (CCF A, ICORE A, CSRankings, Top Conference in Programming Languages)
(with Yichen Tao, Jiawei Chen and Jean-Baptiste Jeannin)

Piecewise Analysis of Probabilistic Programs via k-Induction [Link]
ACM-SIGPLAN Symposium on Principles of Programming Languages
POPL 2026 (CCF A, ICORE A*, CSRankings, Top Conference in Programming Languages)
(with Tengshun Yang, Shenghua Feng, Naijun Zhan, Jingyu Ke and Shiyang Wu)

Structural Abstraction and Refinement for Probabilistic Programs [Link]
ACM SIGPLAN International Conference on Object-Oriented Programming Systems, Languages, and Applications
OOPSLA 2025 (CCF A, ICORE A, CSRankings, Top Conference in Programming Languages)
(with Guanyan Li, Juanen Li, Zhilei Han, Peixin Wang, and Fei He)

Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving [arXiv] [Link]
ACM SIGPLAN Conference on Programming Language Design and Implementation
PLDI 2024 (CCF A, ICORE A*, CSRankings, Top Conference in Programming Languages)
(with Peixin Wang, Tengshun Yang, Guanyan Li and C.-H. Luke Ong)

Automated Tail Bound Analysis for Probabilistic Recurrence Relations [arXiv] [Link]
International Conference on Computer Aided Verification
CAV 2023 (CCF A, ICORE A*, CSRankings, Top Conference in Formal Verification)
(with Yican Sun, Krishnendu Chatterjee and Amir Kafshdar Goharshady)

Quantitative analysis of assertion violations in probabilistic programs [arXiv] [Link]
ACM SIGPLAN International Conference on Programming Language Design and Implementation
PLDI 2021 (CCF A, ICORE A*, CSRankings, Top Conference in Programming Languages)
(with Jinyi Wang, Yican Sun, Krishnendu Chatterjee and Amir Kafshdar Goharshady)

Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time [arXiv] [Link]
ACM SIGPLAN Symposium on Principles of Programming Languages
POPL 2020 (CCF A, ICORE A*, CSRankings, Top Conference in Programming Languages)
(with Peixin Wang, Krishnendu Chatterjee, Yuxin Deng and Ming Xu)

Modular Verification for Almost-Sure Termination of Probabilistic Programs [Link] [arXiv]
ACM SIGPLAN International Conference on Object-Oriented Programming Systems, Languages, and Applications
OOPSLA 2019 (CCF A, ICORE A*, CSRankings, Top Conference in Programming Languages)
(with Mingzhang Huang, Krishnendu Chatterjee and Amir Kafshdar Goharshady)

Cost analysis of nondeterministic probabilistic programs [link] [arXiv]
ACM SIGPLAN Conference on Programming Language Design and Implementation
PLDI 2019 (CCF A, ICORE A*, CSRankings, Top Conference in Programming Languages)
(with Peixin Wang, Amir Kafshdar Goharshady, Krishnendu Chatterjee, Xudong Qin and Wenjun Shi)

Termination of Nondeterministic Probabilistic Programs [link] [arXiv]
International Conference on Verification, Model Checking, and Abstract Interpretation
VMCAI 2019 (CCF B, ICORE B)
(with Krishnendu Chatterjee)

Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs [link]
ACM Transactions on Programming Languages and Systems
TOPLAS 2018 (CCF A, Top Journal in Programming Languages)
(with Krishnendu Chatterjee, Petr Novotny and Rouzbeh Hasheminezhad)
Extended journal version of the conference paper:
- Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs [link] [arXiv]
- ACM SIGPLAN Symposium on Principles of Programming Languages
  POPL 2016 (CCF A, ICORE A*, CSRankings, Top Conference in Programming Languages)

New Approaches for Almost-Sure Termination of Probabilistic Programs [link] [arXiv]
Asian Symposium on Programming Languages and Systems
APLAS 2018 (CCF C, ICORE B)
(with Mingzhang Huang and Krishnendu Chatterjee)

Computational Approaches for Stochastic Shortest Path on Succinct MDPs [link] [arXiv]
International Joint Conference on Artificial Intelligence
IJCAI 2018 (CCF A, ICORE A*, CSRankings )
(with Krishnendu Chatterjee, Amir Kafshdar Goharshady and Nastaran Okati)

Automated Recurrence Analysis for Almost-Linear Expected-Runtime Bounds [link] [arXiv]
International Conference on Computer Aided Verification
CAV 2017 (CCF A, ICORE A*, CSRankings, Top Conference in Formal Verification)
(with Krishnendu Chatterjee and Aniket Murhekar)

Termination Analysis of Probabilistic Programs Through Positivstellensatz's [link] [arXiv]
International Conference on Computer Aided Verification
CAV 2016 (CCF A, ICORE A*, CSRankings, Top Conference in Formal Verification)
(with Krishnendu Chatterjee and Amir Kafshdar Goharshady

Software Verification

Staged Multi-Step UTXO Workflows via Recursive Invariants
ACM SIGPLAN International Conference on Object-Oriented Programming Systems, Languages, and Applications
OOPSLA 2026, to appear (CCF A, ICORE A, CSRankings, Top Conference in Programming Languages)
(with Shuyang Tang, Sherman S. M. Chow, Hongfei Fu, Zihan Guo and Guoqiang Li)

Polynomial Invariant Generation for Floating Point Programs
International Conference on Computer Aided Verification
CAV 2026, to appear (CCF A, ICORE A*, CSRankings, Top Conference in Formal Verification)
(with Xuran Cai and Liqian Chen)

Array-Carrying Symbolic Execution for Function Contract Generation
International Symposium on Formal Methods
FM 2026, to appear (CCF A, ICORE B)
(with Weijie Lu, Jingyu Ke, Zhouyue Sun, Yi Zhou, Guoqiang Li and Haokun Li)

Affine Disjunctive Invariant Generation with Farkas' Lemma [Link]
International Conference on Verification, Model Checking, and Abstract Interpretation
VMCAI 2025 (CCF B, ICORE B)
(with Jingyu Ke, Hongming Liu, Zhouyue Sun, Liqian Chen and Guoqiang Li)

Constraint Based Invariant Generation with Modular Operations [Link]
International Symposium on Dependable Software Engineering. Theories, Tools, and Applications
SETTA 2024 (CCF C)
(with Yuchen Li, Haowen Long and Guoqiang Li)

Demystifying Template-Based Invariant Generation for Bit-Vector Programs [Link]
IEEE/ACM International Conference on Automated Software Engineering
ASE 2023 (CCF A, ICORE A*, CSRankings)
(with Peisen Yao, Jingyu Ke, Jiahui Sun, Rongxin Wu and Kui Ren)

Scalable Linear Invariant Generation with Farkas' Lemma [HAL] [Link]
ACM SIGPLAN International Conference on Object-Oriented Programming Systems, Languages, and Applications
OOPSLA 2022 (CCF A, ICORE A, CSRankings, Top Conference in Programming Languages)
(with Hongming Liu, Zhiyong Yu, Jiaxin Song, Guoqiang Li)

Affine Loop Invariant Generation via Matrix Algebra [HAL] [Link]
International Conference on Computer Aided Verification
CAV 2022 (CCF A, ICORE A*, CSRankings,Top Conference in Formal Verification)
(with Yucheng Ji, Bin Fang and Haibo Chen)

Polynomial reachability witnesses via Stellensaetze [HAL] [Link]
ACM SIGPLAN International Conference on Programming Language Design and Implementation
PLDI 2021 (CCF A, ICORE A*, CSRankings, Top Conference in Programming Languages)
(with Ali Asadi, Prof. Krishnendu Chatterjee, Amir Kafshdar Goharshady and Mohammad Mahdavi)

Polynomial invariant generation for non-deterministic recursive programs [arXiv] [Link]
ACM SIGPLAN International Conference on Programming Language Design and Implementation
PLDI 2020 (CCF A, ICORE A*, CSRankings, Top Conference in Programming Languages)
(with Krishnendu Chatterjee, Amir Kafshdar Goharshady and Ehsan Kafshdar Goharshady)

Non-polynomial Worst-Case Analysis of Recursive Programs [link]
ACM Transactions on Programming Languages and Systems
TOPLAS 2019 (CCF A, Top Journal in Programming Languages)
(with Krishnendu Chatterjee and Amir Kafshdar Goharshady)
Extended journal version of the conference paper:
- Non-polynomial Worst-Case Analysis of Recursive Programs [link] [arXiv]
- International Conference on Computer Aided Verification
  CAV 2017 (CCF A, ICORE A*, CSRankings, Top Conference in Formal Verification)

Formal Models and Complexity

A Formal Approach to Multi-Layered Privileges for Enclaves [Link]
Annual Network and Distributed System Security Symposium. NDSS 2025
(CCF A, ICORE A*, CSRankings)
(with Ganxiang Yang, Chenyang Liu, Zhen Huang, Guoxing Chen, Yuanyuan Zhang and Haojin Zhu)

Deciding Probabilistic Simulation between Probabilistic Pushdown Automata and Finite-State Systems [link]
Information and Computation
IANDC 2019 (CCF A)
(with Mingzhang Huang and Joost-Pieter Katoen)
Extended journal version of the conference paper:
- Deciding Probabilistic Simulation between Probabilistic Pushdown Automata and Finite-State Systems [link]
- IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science
  FSTTCS 2011 (CCF C)

Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties [link] [arXiv]
International Conference on Quantitative Evaluation of Systems
QEST 2018
(with Yi Li and Jianlin Li)

Maximal Cost-Bounded Reachability Probability on Continuous-Time Markov Decision Processes [link] [arXiv]
International Conference on Foundations of Software Science and Computation Structures
FoSSaCS 2014 (CCF B, ICORE B)
(single-author paper)

Approximating acceptance probabilities of CTMC-paths on multi-clock deterministic timed automata [link] [arXiv]
International Conference on Hybrid systems: Computation and Control
HSCC 2013 (CCF B)
(single-author paper, Best Student Paper Award)

Computing Game Metrics on Markov Decision Processes [link] [Full Version]
International Colloquium on Automata, Languages, and Programming
ICALP 2012 Track B (CCF B, ICORE A, Top Conference in Logic and Automata)
(single-author paper)

Model Checking EGF on Basic Parallel Processes [link]
International Symposium on Automated Technology for Verification and Analysis
ATVA 2011 (CCF C, ICORE B)
(single-author paper)

Branching Bisimilarity between Finite-State Systems and BPA or Normed BPP Is Polynomial-Time Decidable [link]
Asian Symposium on Programming Languages and Systems
APLAS 2009 (CCF C, ICORE B)
(single-author paper)

Other Publications

Probabilistic Verification of Neural Networks via Efficient Probabilistic Hull Generation
Conference on Uncertainty in Artificial Intelligence
UAI 2026, to appear (CCF B, ICORE A)
(with Jingyang Li, Xin Chen and Guoqiang Li)

ZKWASM: A ZKSNARK WASM Emulator
IEEE Transactions on Services Computing
TSC 2024 (CCF A)
(with Sinka Gao and Guoqiang Li)

Repo4QA: Answering Coding Questions via Dense Retrieval on GitHub Repositories
International Conference on Computational Linguistics
COLING 2022 (CCF B, ICORE B)
(with Minyu Chen, Guoqiang Li, Chen Ma and Jingyang Li)

Decidability of Behavioral Equivalences in Process Calculi with Name Scoping [link]
IPM International Conference on Fundamentals of Software Engineering
FSEN 2011
(with Chaodong He and Yuxi Fu)

Last updated: May. 7th, 2026