Hongfei Fu (in Chinese: ·ûºè·É)
Assistant Professor at the John Hopcroft Center for Computer Science, Shanghai Jiao Tong University.
Contact:
 Email: "fuhf"+"at"+"cs.sjtu.edu.cn"
 Office: Room 14081, Software Expert Building, Shanghai Jiao Tong University
 Post: Room 14081, Software Expert Building, No. 800 Dongchuan Road, Minhang District, Shanghai 200240, China
Research Interest
I am mainly interested in formal methods, a theoretical research area aiming at proving system correctness through rigorous mathematical approaches. Currently, I am interested in the following subareas of formal methods:
 Program Verification
 Model Checking
PhD Thesis
Verifying Probabilistic Systems: New Algorithms and Complexity Results [link], RWTH Aachen, Germany
Teaching
 Foundations of Programming Languages (Spring 2018, graduate course)
 Discrete Mathematics (Fall 2018, bachelor course)
 Foundations of Programming Languages (Spring 2019, graduate course)
 Discrete Mathematics (Fall 2019, bachelor course)
 Sep. 17th: Lecture 1, Homework, Solution
 Sep. 24th: Lecture 2, Homework, Solution
 Sep. 27th: Lecture 3, Homework, Solution
 Oct. 8th: Lecture 4, Homework, Solution
 Oct. 11th: Lecture 5
 Oct. 12th: Lecture 6, Homework, Solution
 Oct. 15th: Lecture 7, Homework, Solution, Script
 Oct. 22nd: Lecture 8, Homework, Solution
 Oct. 25th: Lecture 9, Homework, Solution
 Oct. 29th: Lecture 10, Homework, Solution
 Nov. 8th: Lecture 11, Homework, Solution
 Nov. 9th: Lecture 12, Homework, Solution, Script
 Nov. 12th: Lecture 13, Homework, Solution
 Nov. 19th: Lecture 14, Homework, Solution, Script
 Nov. 22nd: Lecture 15, Homework, Solution, Script
 Nov. 26th: Lecture 16, Homework, Solution, Script
 Dec. 3rd: Lecture 17, Homework, Solution, Script, Proof(by Prof. Michael Brudno)
 Dec. 6th: Lecture 18, Homework, Solution
 Dec. 10th: Review 1
 Dec. 17th: Review 2
 Dec. 20th: Polya's Counting Theorem(by Prof. Alan Frieze)
 Dec. 24th: Some Number Theory
Publications

Proving Expected Sensitivity of Probabilistic Programs with Randomized VariableDependent Termination Time [arXiv] [Link]
Proceedings of the 47th Annual ACM SIGPLANSIGACT 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)
 Nonpolynomial WorstCase 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:
 Nonpolynomial WorstCase 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 AlmostSure Termination of Probabilistic Programs [Link] [arXiv] [Full Version]
ACM SIGPLAN International Conference on ObjectOriented 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 FiniteState Systems [link]
Information and Computation IANDC 2019 (CCF Rank A)
(with Mingzhang Huang and Prof. JoostPieter Katoen)
Extended journal version of the conference paper:
 Deciding Probabilistic Simulation between Probabilistic Pushdown Automata and FiniteState 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 SIGPLANSIGACT Symposium on Principles of Programming Languages
POPL 2016 (CCF Rank A, Top Conference in Programming Languages)
 New Approaches for AlmostSure 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 TwentySeventh 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 OmegaRegular DenseTime Properties [link] [arXiv]
Quantitative Evaluation of Systems  15th International Conference QEST 2018
(with Yi Li and Jianlin Li)
 Automated Recurrence Analysis for AlmostLinear ExpectedRuntime 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 CostBounded Reachability Probability on ContinuousTime Markov Decision Processes [link] [arXiv]
Foundations of Software Science and Computation Structures  17th International Conference FoSSaCS 2014 (CCF Rank B)
(singleauthor paper)
 Approximating acceptance probabilities of CTMCpaths on multiclock deterministic timed automata [link] [arXiv]
Proceedings of the 16th international conference on Hybrid systems: computation and control HSCC 2013 (CCF Rank B)
(singleauthor 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)
(singleauthor paper)
 Model Checking EGF on Basic Parallel Processes [link]
Automated Technology for Verification and Analysis, 9th International Symposium ATVA 2011 (CCF Rank C)
(singleauthor 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 FiniteState Systems and BPA or Normed BPP Is PolynomialTime Decidable [link]
Programming Languages and Systems, 7th Asian Symposium APLAS 2009 (CCF Rank C)
(singleauthor paper)