贺飞｜清华大学｜学者主页

2026

Deagle for SV-COMP 2027

Zhihang Sun, P Wang, Zhiheng Cai, Fei He

Zenodo (CERN European Organization for Nuclear Research)

DOI

2026

Precise and Efficient Static Data Race Detection

P Wang, Zhihang Sun, Fei He

IEEE/ACM International Conference on Automated Software Engineering (ASE)

DOI

2026

The artifacts of DEAGLE-DL

Pei Wang, Zhilei Han, Zhihang Sun, He Fei

Zenodo (CERN European Organization for Nuclear Research)

DOI

2026

CertiCoder: Towards MISRA-Compliant C Code Generation with LLMs

Min Gou, Zhiyu Yao, Hualong Ma, Ende Zhang, Jie Zhou, Fei He

Proceedings of the ACM on software engineering.

DOI

2026

Accurate Inference of Termination Conditions

Biting Huang, Zhilei Han, Fei He

IEEE/ACM International Conference on Software Engineering (ICSE)

DOI

2026

Learning Symmetric Invariants from Symmetric Samples

Zhijie Xu, Fei He

Proceedings of the ACM on Programming Languages

DOI

2026

Deadlock Verification via Ordering-Constrained Mutex Modeling

P Wang, Zhilei Han, Zhihang Sun, Fei He

Lecture notes in computer science

DOI

2025

Structural Abstraction and Refinement for Probabilistic Programs

Guanyan Li, Jiayu Li, Zhilei Han, Peixin Wang, Hongfei Fu, Fei He

Proceedings of the ACM on Programming Languages

DOI

2023

一种基于变量隐藏抽象的IC3硬件验证算法

杨柳，范洪宇，李东方，贺飞

《计算机科学》

2023

Satisfiability Modulo Ordering Consistency Theory for SC, TSO, and PSO Memory Models

Hongyu Fan, Zhihang Sun, Fei He

ACM Transactions on Programming Languages and Systems

DOI

2023

P4b: A Translator from P4 Programs to Boogie

Chong Ye, Fei He

ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE)

DOI

2023

Automated Ambiguity Detection in Layout-Sensitive Grammars

Jiangyi Liu, Fengmin Zhu, Fei He

Proceedings of the ACM on Programming Languages

DOI

2023

Data-driven Recurrent Set Learning For Non-termination Analysis

Zhilei Han, Fei He

IEEE/ACM International Conference on Software Engineering (ICSE)

DOI

2022

Consistency-preserving propagation for SMT solving of concurrent program verification

Zhihang Sun, Hongyu Fan, Fei He

Proceedings of the ACM on Programming Languages

DOI

2022

Data-driven loop bound learning for termination analysis

Rongchen Xu, Jianhui Chen, Fei He

Proceedings/Proceedings - International Conference on Software Engineering

DOI

2022

Interference relation-guided SMT solving for multi-threaded program verification

Hongyu Fan, Weiting Liu, Fei He

ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming

DOI

2022

Deagle: An SMT-based Verifier for Multi-threaded Programs (Competition Contribution)

Fei He, Zhihang Sun, Hongyu Fan

Lecture notes in computer science

DOI

2021

Satisfiability modulo ordering consistency theory for multi-threaded program verification

Fei He, Zhihang Sun, Hongyu Fan

DOI

2021

Leveraging Control Flow Knowledge in SMT Solving of Program Verification

Jianhui Chen, Fei He

ACM Transactions on Software Engineering and Methodology

DOI

2020

Proving termination by k -induction

Jianhui Chen, Fei He

IEEE/ACM International Conference on Automated Software Engineering (ASE)

DOI

2020

Incremental predicate analysis for regression verification

Qianshan Yu, Fei He, Bow-Yaw Wang

Proceedings of the ACM on Programming Languages

DOI

2020

Termination analysis for evolving programs: an incremental approach by reusing certified modules

Fei He, Jitao Han

Proceedings of the ACM on Programming Languages

DOI

2020

Interval counterexamples for loop invariant learning

Rongchen Xu, Fei He, Bow-Yaw Wang

ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE)

DOI

2020

Proving almost-sure termination by omega-regular decomposition

Jianhui Chen, Fei He

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation

DOI

2018

Control flow-guided SMT solving for program verification

Jianhui Chen, Fei He

IEEE/ACM International Conference on Automated Software Engineering (ASE)

DOI

2018

Efficient software product-line model checking using induction and a SAT solver

Fei He, Yuan Gao, Liangze Yin

Frontiers of Computer Science

DOI

2018

SMT-based query tracking for differentially private data analytics systems

Chen Luo, Fei He

Frontiers of Computer Science

DOI

2017

PSpec: A Formal Specification Language for Fine-Grained Control on Distributed Data Analytics

Chen Luo, Fei He, Dong Yan, Dan Zhang, Xin Zhou, Bow-Yaw Wang

IEEE/ACM International Conference on Software Engineering: Companion Proceedings (ICSE-Companion)

DOI

2017

Inferring software behavioral models with MapReduce

Chen Luo, Fei He, Carlo Ghezzi

Science of Computer Programming

DOI

2016

Learning-Based Assume-Guarantee Regression Verification

Fei He, Shu Mao, Bow-Yaw Wang

Lecture notes in computer science

DOI

2015

基于接口自动机与符号执行的嵌入式软件测试用例生成

王博，白晓颖，张超，贺飞，SONG Xiao-Yu

《计算机学报》

2015

Deadlock detection in FPGA design: A practical approach

Dexi Wang, Fei He, Yangdong Steve Deng, Chao Su, Ming Gu, Jiaguang Sun

Tsinghua Science & Technology

DOI

2015

VeRV: A temporal and data-concerned verification framework for the vehicle bus systems

Shuo Zhang, Fei He, Ming Gu

DOI

2014

运行时验证技术的研究进展

张硕，贺飞

《计算机科学》

2014

Leveraging Weighted Automata in Compositional Reasoning about Concurrent Probabilistic Systems

Fei He, Xiaowei Gao, Bow-Yaw Wang, Lijun Zhang

ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)

DOI

2014

Generalized interface automata with multicast synchronization

Fei He, Xiaoyu Song B, Ming Gu, Jiaguang Sun

Frontiers of Computer Science

DOI

2014

Clause Replication and Reuse in Incremental Temporal Induction

Liangze Yin, Fei He, Ming Gu, Jiaguang Sun

International Conference on Engineering of Complex Computer Systems

DOI

2014

Estimating the Volume of Solution Space for Satisfiability Modulo Linear Real Arithmetic

Min Qi Zhou, Fei He, Xiaoyu Song B, He Shi, Gangyi Chen, Ming Gu

Theory of Computing Systems

DOI

2014

Symbolic assume-guarantee reasoning through BDD learning

Fei He, Bow-Yaw Wang, Liangze Yin, Lei Zhu

Proceedings/Proceedings - International Conference on Software Engineering

DOI

2014

Safety verification of semi-algebraic dynamical systems via inductive invariant

Hui Kong, Fei He, Xiaoyu Song B, Ming Gu, Hongyan Tan, Jiaguang Sun

Tsinghua Science & Technology

DOI

2014

Automated Generation of Instruction Set Simulator from Specification

Vania Joloboff, Shengpeng Liu, Fei He

HAL (Le Centre pour la Communication Scientifique Directe)

2013

Optimizing the SAT Decision Ordering of Bounded Model Checking by Structural Information

Liangze Yin, Fei He, Ming Gu

International Symposium on Theoretical Aspects of Software Engineering (TASE)

DOI

2013

Reusing Search Tree for Incremental SAT Solving of Temporal Induction

Liangze Yin, Fei He, Min Qi Zhou, Ming Gu

International Conference on Engineering of Complex Computer Systems

DOI

2013

Exponential-Condition-Based Barrier Certificate Generation for Safety Verification of Hybrid Systems

Hui Kong, Fei He, Xiaoyu Song B, William N. N. Hung, Ming Gu

Lecture notes in computer science

DOI

2013

VCS: A Verifier for Component-Based Systems

Fei He, Liangze Yin, Bow-Yaw Wang, Lianyi Zhang, Guanyu Mu, Wenrui Meng

Lecture notes in computer science

DOI

2013

A Unified Framework for DPLL(T) + Certificates

Min Qi Zhou, Fei He, Bow-Yaw Wang, Ming Gu, Jiaguang Sun

Journal of Applied Mathematics

DOI

2012

Thread-Modular Model Checking with Iterative Refinement

Wenrui Meng, Fei He, Bow-Yaw Wang, Qiang Liu

Lecture notes in computer science

DOI

2010

Maxterm Covering for Satisfiability

Liangze Yin, Fei He, William N. N. Hung, Xiaoyu Song B, Ming Gu

IEEE Transactions on Computers

DOI

2010

Compositional Abstraction Refinement for Timed Systems

Fei He, He Zhu, William N. N. Hung, Xiaoyu Song B, Ming Gu

DOI

2010

Comparing Learning Algorithms in Automated Assume-Guarantee Reasoning

Yu‐Fang Chen, Edmund M. Clarke, Azadeh Farzan, Fei He, Ming-Hsien Tsai, Yih-Kuen Tsay, Bow-Yaw Wang, Lei Zhu

Lecture notes in computer science

DOI

2010

On Array Theory of Bounded Elements

Min Qi Zhou, Fei He, Bow-Yaw Wang, Ming Gu

Lecture notes in computer science

DOI

2009

Data mining based decomposition for assume-guarantee reasoning

He Zhu, Fei He, William N. N. Hung, Xiaoyu Song B, Ming Gu

Formal Methods in Computer-Aided Design

DOI

2009

Integrating Evolutionary Computation with Abstraction Refinement for Model Checking

Fei He, Xiaoyu Song B, William N. N. Hung, Ming Gu, Jiaguang Sun

IEEE Transactions on Computers

DOI

2009

Translation-Based Model Checking for PLC Programs

Min Qi Zhou, Fei He, Ming Gu, Xiaoyu Song B

DOI

2007

A satisfiability formulation for FPGA routing with pin rearrangements

Fei He, William N. N. Hung, Xiaoyu Song B, Musong Gu, Jun Sun

International Journal of Electronics

DOI

2007

Effective heuristics for counterexample-guided abstraction refinement

Fei He, Xiaoyu Song B, Ming Gu, Jiaguang Sun

ACM Great Lakes Symposium on VLSI (GLSVLSI)

DOI

2007

Formal Analysis of Publish-Subscribe Systems by Probabilistic Timed Automata

Fei He, Luciano Baresi, Carlo Ghezzi, Paola Spoletini

Lecture notes in computer science

DOI

2006

Probabilistic optimization for FPGA board level routing problems

Fei He, Xiaoyu Song B, Ming Gu, Guowu Yang, William N. N. Hung, Jiaguang Sun

IEEE Transactions on Circuits and Systems II Analog and Digital Signal Processing

DOI

2006

Verifying Java Programs By Theorem Prover HOL

Anduo Wang, Fei He, Ming Gu, Xiaoyu Song B

IEEE Annual International Computer Software and Applications Conference (COMPSAC)

DOI

2006

A Probabilistic Learning Approach for Counterexample Guided Abstraction Refinement

Fei He, Xiaoyu Song B, Ming Gu, Jiaguang Sun

Lecture notes in computer science

DOI

2005

Segment Channel Routing with Pin Rearrangements via Satisfiability

Fei He, William N. N. Hung, Xiaoyu Song B, Ming Gu, Jiaguang Sun

IEEE International Symposium on Circuits and Systems proceedings

DOI

精选作品

期刊论文

Deagle for SV-COMP 2027

Precise and Efficient Static Data Race Detection

The artifacts of DEAGLE-DL

CertiCoder: Towards MISRA-Compliant C Code Generation with LLMs

Accurate Inference of Termination Conditions

Learning Symmetric Invariants from Symmetric Samples

Deadlock Verification via Ordering-Constrained Mutex Modeling

Structural Abstraction and Refinement for Probabilistic Programs

一种基于变量隐藏抽象的IC3硬件验证算法

Satisfiability Modulo Ordering Consistency Theory for SC, TSO, and PSO Memory Models

P4b: A Translator from P4 Programs to Boogie

Automated Ambiguity Detection in Layout-Sensitive Grammars

Data-driven Recurrent Set Learning For Non-termination Analysis

Consistency-preserving propagation for SMT solving of concurrent program verification

Data-driven loop bound learning for termination analysis

Interference relation-guided SMT solving for multi-threaded program verification

Deagle: An SMT-based Verifier for Multi-threaded Programs (Competition Contribution)

Satisfiability modulo ordering consistency theory for multi-threaded program verification

Leveraging Control Flow Knowledge in SMT Solving of Program Verification

Proving termination by k -induction

Incremental predicate analysis for regression verification

Termination analysis for evolving programs: an incremental approach by reusing certified modules

Interval counterexamples for loop invariant learning

Proving almost-sure termination by omega-regular decomposition

Control flow-guided SMT solving for program verification

Efficient software product-line model checking using induction and a SAT solver

SMT-based query tracking for differentially private data analytics systems

PSpec: A Formal Specification Language for Fine-Grained Control on Distributed Data Analytics

Inferring software behavioral models with MapReduce

Learning-Based Assume-Guarantee Regression Verification

基于接口自动机与符号执行的嵌入式软件测试用例生成

Deadlock detection in FPGA design: A practical approach

VeRV: A temporal and data-concerned verification framework for the vehicle bus systems

运行时验证技术的研究进展

Leveraging Weighted Automata in Compositional Reasoning about Concurrent Probabilistic Systems

Generalized interface automata with multicast synchronization

Clause Replication and Reuse in Incremental Temporal Induction

Estimating the Volume of Solution Space for Satisfiability Modulo Linear Real Arithmetic

Symbolic assume-guarantee reasoning through BDD learning

Safety verification of semi-algebraic dynamical systems via inductive invariant

Automated Generation of Instruction Set Simulator from Specification

Optimizing the SAT Decision Ordering of Bounded Model Checking by Structural Information

Reusing Search Tree for Incremental SAT Solving of Temporal Induction

Exponential-Condition-Based Barrier Certificate Generation for Safety Verification of Hybrid Systems

VCS: A Verifier for Component-Based Systems

A Unified Framework for DPLL(T) + Certificates

Thread-Modular Model Checking with Iterative Refinement

Maxterm Covering for Satisfiability

Compositional Abstraction Refinement for Timed Systems

Comparing Learning Algorithms in Automated Assume-Guarantee Reasoning

On Array Theory of Bounded Elements

Data mining based decomposition for assume-guarantee reasoning

Integrating Evolutionary Computation with Abstraction Refinement for Model Checking

Translation-Based Model Checking for PLC Programs

A satisfiability formulation for FPGA routing with pin rearrangements

Effective heuristics for counterexample-guided abstraction refinement

Formal Analysis of Publish-Subscribe Systems by Probabilistic Timed Automata

Probabilistic optimization for FPGA board level routing problems

Verifying Java Programs By Theorem Prover HOL

A Probabilistic Learning Approach for Counterexample Guided Abstraction Refinement

Segment Channel Routing with Pin Rearrangements via Satisfiability

预印本

Leveraging Datapath Propagation in IC3 for Hardware Model Checking

ProbTA: A sound and complete proof rule for probabilistic verification

When Regression Verification Meets CEGAR

研究方向