Branching Bisimilarity between Finite-State Systems and BPA or Normed BPP Is Polynomial-Time Decidable. - Hongfei Fu 001 (APLAS, 2009)

Model Checking EGF on Basic Parallel Processes. - Hongfei Fu 001 (ATVA, 2011)

Decidability of Behavioral Equivalences in Process Calculi with Name Scoping. - Chaodong He; Yuxi Fu; Hongfei Fu 001 (FSEN, 2011)

Deciding Probabilistic Simulation between Probabilistic Pushdown Automata and Finite-State Systems. - Hongfei Fu 001; Joost-Pieter Katoen (FSTTCS, 2011)

Computing Game Metrics on Markov Decision Processes. - Hongfei Fu 001 (ICALP (2), 2012)

Approximating acceptance probabilities of CTMC-paths on multi-clock deterministic timed automata. - Hongfei Fu 001 (HSCC, 2013)

Maximal Cost-Bounded Reachability Probability on Continuous-Time Markov Decision Processes. - Hongfei Fu 001 (FoSSaCS, 2014)

Verifying probabilistic systems: new algorithms and complexity results. - Hongfei Fu 001 (2014)

Termination Analysis of Probabilistic Programs Through Positivstellensatz's. - Krishnendu Chatterjee; Hongfei Fu 001; Amir Kafshdar Goharshady (CAV (1), 2016)

Automated Recurrence Analysis for Almost-Linear Expected-Runtime Bounds. - Krishnendu Chatterjee; Hongfei Fu 001; Aniket Murhekar (CAV (1), 2017)

Termination of Nondeterministic Recursive Probabilistic Programs. - Krishnendu Chatterjee; Hongfei Fu 001 (CoRR, 2017)

Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties. - Hongfei Fu 001; Yi Li; Jianlin Li; Lijun Zhang 001 (CoRR, 2017)

New Approaches for Almost-Sure Termination of Probabilistic Programs. - Mingzhang Huang; Hongfei Fu 001; Krishnendu Chatterjee (APLAS, 2018)

Computational Approaches for Stochastic Shortest Path on Succinct MDPs. - Krishnendu Chatterjee; Hongfei Fu 001; Amir Kafshdar Goharshady; Nastaran Okati (IJCAI, 2018)

Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties. - Hongfei Fu 001; Yi Li; Jianlin Li (QEST, 2018)

Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs. - Krishnendu Chatterjee; Hongfei Fu 001; Petr Novotný 001; Rouzbeh Hasheminezhad (ACM Trans. Program. Lang. Syst., 2018)

Cost analysis of nondeterministic probabilistic programs. - Peixin Wang; Hongfei Fu 001; Amir Kafshdar Goharshady; Krishnendu Chatterjee; Xudong Qin; Wenjun Shi (PLDI, 2019)

Termination of Nondeterministic Probabilistic Programs. - Hongfei Fu 001; Krishnendu Chatterjee (VMCAI, 2019)

Compositional Analysis for Almost-Sure Termination of Probabilistic Programs. - Mingzhang Huang; Hongfei Fu 001; Krishnendu Chatterjee; Amir Kafshdar Goharshady (CoRR, 2019)

Proving Expected Sensitivity of Probabilistic Programs with Randomized Execution Time. - Peixin Wang; Hongfei Fu 001; Krishnendu Chatterjee; Kangli He; Ming Xu 010 (CoRR, 2019)

Deciding probabilistic simulation between probabilistic pushdown automata and finite-state systems. - Mingzhang Huang; Hongfei Fu 001; Joost-Pieter Katoen (Inf. Comput., 2019)

Modular verification for almost-sure termination of probabilistic programs. - Mingzhang Huang; Hongfei Fu 001; Krishnendu Chatterjee; Amir Kafshdar Goharshady (Proc. ACM Program. Lang., 2019)

Non-polynomial Worst-Case Analysis of Recursive Programs. - Krishnendu Chatterjee; Hongfei Fu 001; Amir Kafshdar Goharshady (ACM Trans. Program. Lang. Syst., 2019)

Termination Analysis of Probabilistic Programs with Martingales. - Krishnendu Chatterjee; Hongfei Fu 001; Petr Novotný 001 (Foundations of Probabilistic Programming, 2020)

Polynomial invariant generation for non-deterministic recursive programs. - Krishnendu Chatterjee; Hongfei Fu 001; Amir Kafshdar Goharshady; Ehsan Kafshdar Goharshady (PLDI, 2020)

Inductive Reachability Witnesses. - Ali Asadi; Krishnendu Chatterjee; Hongfei Fu 001; Amir Kafshdar Goharshady; Mohammad Mahdavi (CoRR, 2020)

Concentration-Bound Analysis for Probabilistic Programs and Probabilistic Recurrence Relations. - Jinyi Wang; Yican Sun; Hongfei Fu 001; Mingzhang Huang; Amir Kafshdar Goharshady; Krishnendu Chatterjee (CoRR, 2020)

Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time. - Peixin Wang; Hongfei Fu 001; Krishnendu Chatterjee; Yuxin Deng; Ming Xu 010 (Proc. ACM Program. Lang., 2020)

Polynomial reachability witnesses via Stellensätze. - Ali Asadi; Krishnendu Chatterjee; Hongfei Fu 001; Amir Kafshdar Goharshady; Mohammad Mahdavi (PLDI, 2021)

Quantitative analysis of assertion violations in probabilistic programs. - Jinyi Wang; Yican Sun; Hongfei Fu 001; Krishnendu Chatterjee; Amir Kafshdar Goharshady (PLDI, 2021)

Affine Loop Invariant Generation via Matrix Algebra. - Yucheng Ji; Hongfei Fu 001; Bin Fang; Haibo Chen 001 (CAV (1), 2022)

Repo4QA: Answering Coding Questions via Dense Retrieval on GitHub Repositories. - Minyu Chen; Guoqiang Li 001; Chen Ma; Jingyang Li; Hongfei Fu 001 (COLING, 2022)

Guided Diffusion Model for Adversarial Purification. - Jinyi Wang; Zhaoyang Lyu; Dahua Lin; Bo Dai 002; Hongfei Fu 001 (CoRR, 2022)

Scalable linear invariant generation with Farkas' lemma. - Hongming Liu; Hongfei Fu 001; Zhiyong Yu; Jiaxin Song; Guoqiang Li 001 (Proc. ACM Program. Lang., 2022)

Automated Tail Bound Analysis for Probabilistic Recurrence Relations. - Yican Sun; Hongfei Fu 001; Krishnendu Chatterjee; Amir Kafshdar Goharshady (CAV (3), 2023)

Demystifying Template-Based Invariant Generation for Bit-Vector Programs. - Peisen Yao; Jingyu Ke; Jiahui Sun; Hongfei Fu 001; Rongxin Wu; Kui Ren 001 (ASE, 2023)

Template-Based Static Posterior Inference for Bayesian Probabilistic Programming. - Peixin Wang; Hongfei Fu 001; Tengshun Yang; Guanyan Li; Luke Ong (CoRR, 2023)

Affine Disjunctive Invariant Generation with Farkas' Lemma. - Hongming Liu; Jingyu Ke; Hongfei Fu 001; Liqian Chen; Guoqiang Li 001 (CoRR, 2023)

Constraint Based Invariant Generation with Modular Operations. - Yuchen Li; Hongfei Fu 001; Haowen Long; Guoqiang Li 001 (SETTA, 2024)

Equational Bit-Vector Solving via Strong Gröbner Bases. - Jiaxin Song; Hongfei Fu 001; Charles Zhang (CoRR, 2024)

Piecewise Linear Expectation Analysis via k-Induction for Probabilistic Programs. - Tengshun Yang; Hongfei Fu 001; Jingyu Ke; Naijun Zhan; Shiyang Wu (CoRR, 2024)

Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving. - Peixin Wang; Tengshun Yang; Hongfei Fu 001; Guanyan Li; C.-H. Luke Ong (Proc. ACM Program. Lang., 2024)

ZKWASM: A ZKSNARK WASM Emulator. - Sinka Gao; Guoqiang Li 001; Hongfei Fu 001 (IEEE Trans. Serv. Comput., 2024)

A Formal Approach to Multi-Layered Privileges for Enclaves. - Ganxiang Yang; Chenyang Liu; Zhen Huang; Guoxing Chen; Hongfei Fu 001; Yuanyuan Zhang; Haojin Zhu (NDSS, 2025)

Affine Disjunctive Invariant Generation with Farkas' Lemma. - Jingyu Ke; Hongfei Fu 001; Hongming Liu; Zhouyue Sun; Liqian Chen; Guoqiang Li 001 (VMCAI (1), 2025)

Invariant Generation for Floating-Point Programs via Constraint Solving. - Xuran Cai; Liqian Chen; Hongfei Fu 001 (CoRR, 2025)

Structural Abstraction and Refinement for Probabilistic Programs. - Guanyan Li; Juanen Li; Zhilei Han; Peixin Wang; Hongfei Fu 001; Fei He 001 (CoRR, 2025)