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 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 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 sub-areas 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)
- Foundations of Programming Languages (Spring 2020, graduate course)
- Program Analysis and Verification (Spring 2020, bachelor course, co-taught with Prof. Yuting Chen)
- Discrete Mathematics (Fall 2020, bachelor course)
Publications
- 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: - 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: - 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)
