Hongfei Fu

Associate Professor (Tenure-Track) at the John Hopcroft Center for Computer Science, Shanghai Jiao Tong University.

Contact:

Email: "fuhf"+"at"+"cs.sjtu.edu.cn"
Office: Room 1408-1, Software Expert Building, Shanghai Jiao Tong University
Post: Room 1408-1, Software Expert Building, No. 800 Dongchuan Road, Minhang District, Shanghai 200240, China

Research Interest

I am interested in formal verification, a theoretical research area that aims at proving system correctness via mathematical methods.

PhD Thesis

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

Teaching

Foundations of Programming Languages (Spring 2018 -- 2021, graduate course)
Discrete Mathematics (Fall 2018 -- 2023, bachelor course)
Program Analysis and Verification (Spring 2020, bachelor course, co-taught with Prof. Yuting Chen)
Model Checking (Spring 2022 -- 2023 , bachelor course)

Manuscripts

Static Analysis of Posterior Inference in Bayesian Probabilistic Programming [PDF] (Feb. 13th, 2023)
Linear Disjunctive Invariant Generation with Farkas' Lemma [PDF] (Nov. 14th, 2022)
ZAWA: A ZKSNARK WASM Emulator [PDF] (Nov. 14th, 2022)

Publications

Probabilistic Verification

Automated Tail Bound Analysis for Probabilistic Recurrence Relations [arXiv] [Link]
Proceedings of the 35th International Conference on Computer Aided Verification
CAV 2023 (CCF Rank A, Top Conference in Formal Verification)
(with Yican Sun, Prof. Krishnendu Chatterjee and Amir Kafshdar Goharshady)

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

Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time [arXiv] [Link]
Proceedings of the 47th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
POPL 2020 (CCF Rank A, Top Conference in Programming Languages)
(with Peixin Wang, Prof. Krishnendu Chatterjee, Prof. Yuxin Deng and Ming Xu)

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

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

Deciding Probabilistic Simulation between Probabilistic Pushdown Automata and Finite-State Systems [link]
Information and Computation IANDC 2019 (CCF Rank A)
(with Mingzhang Huang and Prof. 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 Rank C)

Termination of Nondeterministic Probabilistic Programs [link] [arXiv]
Verification, Model Checking, and Abstract Interpretation - 20th International Conference VMCAI 2019 (CCF Rank B)
(with Prof. 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 Rank A, Top Journal in Programming Languages)
(with Prof. 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]
- Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
  POPL 2016 (CCF Rank A, Top Conference in Programming Languages)

New Approaches for Almost-Sure Termination of Probabilistic Programs [link] [arXiv]
Programming Languages and Systems - 16th Asian Symposium APLAS 2018 (CCF Rank C)
(with Mingzhang Huang and Prof. Krishnendu Chatterjee)

Computational Approaches for Stochastic Shortest Path on Succinct MDPs [link] [arXiv]
Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence IJCAI 2018 (CCF Rank A)
(with Prof. Krishnendu Chatterjee, Amir Kafshdar Goharshady and Nastaran Okati)

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

Automated Recurrence Analysis for Almost-Linear Expected-Runtime Bounds [link] [arXiv]
Computer Aided Verification - 29th International Conference
CAV 2017 (CCF Rank A, Top Conference in Formal Verification )
(with Prof. Krishnendu Chatterjee and Aniket Murhekar)

Termination Analysis of Probabilistic Programs Through Positivstellensatz's [link] [arXiv]
Computer Aided Verification - 28th International Conference
CAV 2016 (CCF Rank A, Top Conference in Formal Verification)
(with Prof. Krishnendu Chatterjee and Amir Kafshdar Goharshady）

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

Approximating acceptance probabilities of CTMC-paths on multi-clock deterministic timed automata [link] [arXiv]
Proceedings of the 16th international conference on Hybrid systems: computation and control HSCC 2013 (CCF Rank B)
(single-author paper, Best Student Paper Award)

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

Invariant/Reachability/Complexity Verification

Demystifying Template-Based Invariant Generation for Bit-Vector Programs [Link]
Proceedings of the 38th IEEE/ACM International Conference on Automated Software Engineering
ASE 2023 (CCF Rank A)
(with Peisen Yao, Jingyu Ke, Jiahui Sun, Rongxin Wu and Prof. Kui Ren)

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

Affine Loop Invariant Generation via Matrix Algebra [HAL] [Link]
Proceedings of the 34th International Conference on Computer Aided Verification
CAV 2022 (CCF Rank A, Top Conference in Formal Verification)
(with Yucheng Ji, Bin Fang and Prof. Haibo Chen)

Polynomial reachability witnesses via Stellensaetze [HAL] [Link]
Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation
PLDI 2021 (CCF Rank A, Top Conference in Programming Languages)
(with Ali Asadi, Prof. Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady, Mohammad Mahdavi)

Polynomial invariant generation for non-deterministic recursive programs [arXiv] [Link]
Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation
PLDI 2020 (CCF Rank A, Top Conference in Programming Languages)
(with Prof. Krishnendu Chatterjee, Amir Kafshdar Goharshady, Ehsan Kafshdar Goharshady)

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

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

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

Miscellaneous

Repo4QA: Answering Coding Questions via Dense Retrieval on GitHub Repositories
Proceedings of the 29th International Conference on Computational Linguistics
COLING 2022 (CCF Rank B)
(with Minyu Chen, Dr. Guoqiang Li, Chen Ma and Jingyang Li, co-supervised by Dr. Guoqiang Li)

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

Last updated: Sep. 23rd, 2023