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

PhD Thesis

Teaching

• Foundations of Programming Languages (Spring 2018 -- 2021, graduate course)
• Discrete Mathematics (Fall 2018 -- 2023, bachelor course, notes under update)
  [Propositional Logic]
  [Propositional Logical Equivalence and Satisfiability]
  [Predicate Logic]
  [Normal Forms]
  [Inference Rules]
  [Basics of Set Theory]
  [Relations]
  [Equivalence Relations and Partial Orders]
  [Closure of Relations]
  [Functions and Equinumerosity]
  [First Order Logic]
  [Basics of Graphs]
  [Bipartite Graphs and Graph Isomorphism]
  [Connectivity, Paths and Circuits]
  [Euler Paths and Circuits]
  [Hamilton Paths and Circuits]
  [Trees]
  [Minimal Spanning Trees]
  [Inclusion-Exclusion Principle]
  [Planar Graphs and Graph Coloring]
  [Huffman Coding]
• Program Analysis and Verification (Spring 2020, bachelor course, co-taught with Prof. Yuting Chen)
• Model Checking (Spring 2022 -- 2023 , bachelor course, notes under update)
  [Background and Mathematical Models]
  [Parallelism and Communication]
  [Linear Time Properties A]
  [Linear Time Properties B]
  [Linear Time Properties C]
  [Finite Automata]
  [Automata on Infinite Words]
  [Model Checking Regular Linear-Time Properties]
  [Linear Temporal Logic A]
  [Linear Temporal Logic B]
  [Linear Temporal Logic C]
  [Linear Temporal Logic D]
  [Computation Tree Logic A]
  [Computation Tree Logic B]
  [Equivalence on Transition Systems]
  [Partition Refinement Algorithms]
  [Partial Order Reduction A]
  [Partial Order Reduction B]
  [Partial Order Reduction C]
  

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)