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

• Program Verification
• Model Checking

PhD Thesis

Teaching

• Foundations of Programming Languages (Spring 2018 -- 2021, graduate course)
• Discrete Mathematics (Fall 2018 -- 2022, 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)
• Automated Tail Bound Analysis for Probabilistic Recurrence Relations [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

• 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)


• 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)


• 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)


• 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)


• 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)


• 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)


• 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)


• 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)


• 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)


• 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)


• 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)