• TrustC: a secure programming language (enhanced C with memory and thread safety)

• Program verification (C programs, GPU programs, concurrent programs under weak memory models), translation verification (e.g., C-to-TrustC translation, compiler verification)

• SMT theories and decision procedures

• Secure and trustworthy code generation

Working Experiences

• Associate Professor, Tsinghua University, 2011.12-Present

• Visiting Scholar, Carnegie Mellon University, 2010.9 - 2011.3

• Assistant Professor, Tsinghua University, 2008.5-2011.12

TOOLS / SOFTWARE

• Beagle: a model checking tool

• Ceagle: a program verification platform for C

• Deagle: a concurrent program verifier (winner of the ConcurrencySafety category at SV-COMP 2022, 2023, and 2025)

SELECTED JOURNAL PUBLICATIONS

• Hongyu Fan, and Fei He, Leveraging Datapath Propagation in IC3 for Hardware Model Checking, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), July 2024, 43(7): 2215-2228.

• Hongyu Fan, Zhihang Sun and Fei He, Satisfiability Modulo Ordering Consistency Theory for SC, TSO, and PSO Memory Models, ACM Transactions on Programming Languages and Systems (TOPLAS), 2023, 45 (1), Article 6, 37 pages.

• Fei He, Qianshan Yu and Liming Cai, Efficient Summary Reuse for Software Regression Verification, IEEE Transactions on Software Engineering, April 2022, 48(4): 1417-1431.

• Jianhui Chen, Fei He, Leveraging Control Flow Knowledge in SMT Solving of Program Verification, ACM Transactions on Software Engineering and Methodology (TOSEM), May 2021, 30 (4), Article 41, 26 pages.

• Chen Luo, Fei He, Fei Peng, Dong Yan, Dan Zhang and Xin Zhou, PSpec-SQL: Enabling Fine-Grained Control for Distributed Data Analytics, IEEE Transactions on Dependable and Secure Computing, 2021, 18 (2): 810-824.

• Fei He, Xiaowei Gao, Miaofei Wang, Bow-Yaw Wang and Lijun Zhang, Learning Weighted Assumptions for Compositional Verification of Markov Decision Processes (extended version of the POPL'15 paper), ACM Transactions on Software Engineering and Methodology (TOSEM), June 2016, 25 (3), Article 21, 39 pages.

• Min Zhou, Fei He, Bow-Yaw Wang, Ming Gu and Jiaguang Sun, Array Theory of Bounded Elements and its Applications, Journal of Automated Reasoning, 52(4), pp. 379-405, April, 2014.

• Liangze Yin, Fei He, William N. N. Hung, Xiaoyu Song and Ming Gu, Maxterm Covering for Satisfiability, IEEE Transactions on Computers, 61(3), pp. 420-426, March, 2012.

• Fei He, Xiaoyu Song, William N. N. Hung, Ming Gu and Jiaguang Sun, Integrating Evolutionary Computation with Abstraction Refinement for Model Checking, IEEE Transactions on Computers, vol. 59, no. 1, pp. 116-126, Jan. 2010.

SELECTED CONFERENCE PUBLICATIONS

• Zhijie Xu and Fei He, Learning Symmetric Invariants from Symmetric Samples, OOPSLA 2026.

• Zhiheng Cai, Zhihang Sun and Fei He, A Refined Ordering Consistency Theory: Full Sequential Consistency and Generalized Preventive Reasoning, FM 2026.

• Min Gou, Zhiyu Yao, Hualong Ma, Ende Zhang, Jian Zhou and Fei He, CertiCoder: Towards MISRA-Compliant C Code Generation with LLMs, FSE 2026.

• Biting Huang, Zhilei Han and Fei He, Accurate Inference of Termination Conditions, ICSE 2026 (ACM Distinguished Paper Award).  

• Guanyan Li, Juanen Li, Zhilei Han, Peixin Wang, Hongfei Fu and Fei He, Structural Abstraction and Refinement for Probabilistic Programs, OOPSLA 2025. 

• Zhilei Han and Fei He, Robustness Verification for Checking Crash Consistency of Non-volatile Memory, ASPLOS 2025. 

• Delong Zhang, Chong Ye and Fei He, On Temporal Verification of Stateful P4 Programs, NSDI 2025. 

• Delong Zhang, Chong Ye and Fei He, P4Inv: Inferring Packet Invariants for Verification of Stateful P4 Programs, INFOCOM 2024. 

• Jiangyi Liu, Fengmin Zhu and Fei He, Automated Ambiguity Detection in Layout-Sensitive Grammars, OOPSLA 2023.  

• Zhilei Han and Fei He, Data-driven Recurrent Set Learning For Non-termination Analysis, ICSE 2023. 

• Fengmin Zhu, Xingyu Xie, Dongyu Feng, Na Meng and Fei He, Mastery: Shifted-Code-Aware Structured Merging, SETTA 2022 (Best Paper Award).

• Zhihang Sun, Hongyu Fan and Fei He. Consistency-Preserving Propagation for SMT Solving of Concurrent Program Verification, OOPSLA 2022. 

• Fei He, Zhihang Sun and Hongyu Fan, Deagle: An SMT-based Verifier for Multi-threaded Programs (Competition Contribution), TACAS 2022. 

• Rongchen Xu, Jianhui Chen and Fei He, Data-Driven Loop Bound Learning for Termination Analysis, ICSE 2022. 

• Hongyu Fan, Weiting Liu and Fei He, Interference Relation-Guided SMT Solving for Multi-Threaded Program Verification, PPoPP 2022 (Best Paper Award).

• Fei He, Zhihang Sun and Hongyu Fan, Satisfiability Modulo Ordering Consistency Theory for Multi-threaded Program Verification, PLDI 2021.

• Fei He and Jitao Han, Termination Analysis for Evolving Programs: an incremental approach by reusing certified modules, OOPSLA 2020.

• Qianshan Yu, Fei He and Bow-Yaw Wang, Incremental Predicate Analysis for Regression Verification, OOPSLA 2020.

• Rongchen Xu, Fei He and Bow-Yaw Wang, Interval Counterexamples for Loop Invariant Learning, ESEC/FSE 2020.

• Jianhui Chen and Fei He, Proving Almost-Sure Termination by Omega-Regular Decomposition, PLDI 2020.

• Jianhui Chen and Fei He, Control Flow-Guided SMT Solving for Program Verification, ASE 2018 (ACM SIGSOFT Distinguished Paper). 

• Fengmin Zhu and Fei He, Conflict Resolution for Structured Merge via Version Space Algebra, OOPSLA 2018.

• Fei He, Xiaowei Gao, Bow-Yaw Wang and Lijun Zhang, Leveraging Weighted Automata in Composition Reasoning about Concurrent Probabilistic Systems, POPL 2015.

• Shuo Zhang, Fei He and Ming Gu, VeRV: A Temporal and Data-Concerned Verification Framework for the Vehicle Bus Systems, IEEE INFOCOM 2015.
  

• Fei He, Bow-Yaw Wang, Liangze Yin, and Lei Zhu, Symbolic Assume-Guarantee Reasoning through BDD Learning, ICSE 2014.  

• Hui Kong, Fei He, Xiaoyu Song, William N. N. Hung and Ming Gu, Exponential-Condition-Based Barrier Certificate Generation for Safety Verification of Hybrid Systems, CAV 2013.

• Min Zhou, Fei He, Bow-Yaw Wang, Ming Gu, On Array Theory of Bounded Elements, CAV 2010.