|
Fei HeAssociate ProfessorSchool of Software Tsinghua University Beijing 100084, China
Office: Room 11-307, East Main Building, Tsinghua University
|
Formal verification, program analysis and decision procedures.
Here is my Publication List
Here is my THUFV lab
I am currently looking for highly motivated postdoctoral and PhD students. All interested candidates are welcome to apply. Kindly send your CV to me via email.
Oct 02, 2024: Our paper, titled "PMVerify: Robustness Verification for Checking Crash Consistency of Non-volatile Memory", was conditionally accepted by ASPLOS 2025.
Jul 24, 2024: Our paper, titled "On Temporal Verification of Stateful P4 Programs", was accepted by NSDI 2025.
Jan 17, 2024: Our paper, titled "Leveraging Datapath Propagation in IC3 for Hardware Model Checking", was accepted by IEEE TCAD.
Dec 01, 2023: Our paper, titled "P4Inv: Inferring Packet Invariants for Verification of Stateful P4 Programs", was accepted by INFOCOM 2024.
Aug 29, 2023: Our paper, titled "Automated Ambiguity Detection in Layout-Sensitive Grammars", was finally accepted by OOPSLA 2023.
Dec 9, 2022: Our paper, titled "Data-driven Recurrent Set Learning For Non-termination Analysis", was accepted by ICSE 2023.
Dec 3, 2022: Our paper, titled "Satisfiability Modulo Ordering Consistency Theory for SC, TSO, and PSO Memory Models", was accepted by ACM TOPLAS.
Oct 28, 2022: Our paper, titled "Mastery: Shifted-Code-Aware Structured Merging", received the Best Paper Award at SETTA 2022!
Jul 1, 2022: Our paper, titled "Consistency-Preserving Propagation for SMT Solving of Concurrent Program Verification", was accepted by OOPSLA 2022.
Apr 18, 2022: Our PPoPP'22 paper, titled "Interference Relation-Guided SMT Solving for Multi-Threaded Program Verification", received the Best Paper Award at PPoPP 2022!
Dec 19, 2021: Our program verification tool Deagle won the gold medal in "ConcurrencySafety" category in SV-COMP 2022!
Dec 3, 2021: Our paper, titled "Data-Driven Loop Bound Learning for Termination Analysis ", was accepted by ICSE 2022.
Nov 16, 2021: Our paper, titled "Interference Relation-Guided SMT Solving for Multi-Threaded Program Verification ", was accepted by PPoPP 2022.
Apr 9, 2021: "Satisfiability Modulo Ordering Consistency Theory for Multi-Threaded Program Verification", was accepted by PLDI 2021.
Dec 26, 2020: "Leveraging Control Flow Knowledge in SMT Solving of Program Verification" was accepted by ACM TOSEM.
Oct 2, 2020: "Termination Analysis for Evolving Programs" and "Incremental Predicate Analysis for Regression Verification" were accepted by OOPSLA 2020.
Aug 21, 2020: "Efficient Summary Reuse for Software Regression Verification" was accepted by IEEE TSE.
Jul 4, 2020: "Proving Termination by k-Induction" was accepted by ASE 2020 (NIER).
May 20, 2020: "Interval Counterexamples for Loop Invariant Learning" was accepted by ESEC/FSE 2020.
Feb 29, 2020: "Proving Almost-Sure Termination by Omega-Regular Decomposition" was accepted by PLDI 2020.
Associate Professor, School of Software, Tsinghua University, 2011.12 - present
Visiting Scholar, Carnegie Mellon University (with Prof. Edmund Clarke), 2010.9 - 2011.3
Assistant Professor, School of Software, Tsinghua University, 2008.5 - 2011.12
Visiting Scholar, Politecnico di Milano (with Prof. Carlo Ghezzi), 2006.11 - 2007.4
Ph.D., Department of Computer Science and Technology, Tsinghua University (advisor Prof. Jiaguang Sun), China, 2008.1
Bachelor, College of Computer, National University of Defense Technology (NUDT), China, 2002.7
Formal verification (graduate course)
Modeling and analysis of embedded computing systems (graduate course)
Associate editor, Theory of Computing Systems, 2021 - present
Young associate editor, Frontiers of Computer Science, 2012 - present
Program committee member (current): ICSE 25', OOPSLA 24'
Program committee member (past): ICSE 23-24', ESEC/FSE 22', FMCAD 20-22' & 16-18', SAT 21-22', ATVA 22', ICTAC 22', FMAC 16-19', CONCUR 18', ATVA 18', MEMCODE 18', SETTA 16-17', ICECCS 17' & 13-15', APLAS 14'
Local Arrangement Chair, ISSTA 19'
Program committee co-Chair: YR-SETTA 17'
Zhihang Sun (PhD student, since 2020)
Zhilei Han (PhD student, since 2021)
Zhijie Xu (PhD student, since 2022)
Biting Huang (PhD student, since 2023)
Pei Wang (PhD student, since 2023)
Yang Zhang (Master student, since 2020)
Xingyu Xie (Master student, since 2021)
Delong Zhang (Master student, since 2022)
Hongyu Fan (PhD 2024, Huawei)
Qianshan Yu (PhD 2022, ZGC Lab)
Jianhui Chen (PhD 2021, Huawei)
Chong Ye (Master 2023, Huawei)
Rongchen Xu (Master 2022, Huawei)
Jitao Han (Master 2021, Huawei)
Liu Yang (Master 2021, Meituan)
Fengmin Zhu (Master 2020, PhD student in MPI-SWS)
Qinyu Wang (Master 2020)
…