A comparative study on search strategies for cell assignments. - Ming Gu 001; Fei He 001; William N. N. Hung; Xiaoyu Song (Int. J. Comput. Math., 2004)

A stochastic model for cellassignments in PCS networks. - Fei He 001; Ming Gu 001; Jiaguang Sun 001; Xiaoyu Song (Math. Comput. Model., 2004)

Segmented channel routing with pin rearrangements via satisfiability. - Fei He 001; William N. N. Hung; Xiaoyu Song; Ming Gu 001; Jiaguang Sun 001 (ISCAS (6), 2005)

A Hierachical Method for Wiring and Congestion Prediction. - Fei He 001; Xiaoyu Song; Lerong Cheng; Guowu Yang; Zhiwei Tang; Ming Gu 001; Jia-Guang Sun 001 (ISVLSI, 2005)

Probabilistic Estimation for Routing Space. - Fei He 001; Ming Gu 001; Xiaoyu Song; Zhiwei Tang; Guowu Yang; Lerong Cheng (Comput. J., 2005)

On Theoretical Upper Bounds for Routing Estimation. - Fei He 001; Lerong Cheng; Guowu Yang; Xiaoyu Song; Ming Gu 001; Jia-Guang Sun 001 (J. Univers. Comput. Sci., 2005)

Multiterminal net assignments by scatter search. - Ming Gu 001; Fei He 001; Xiaoyu Song; Jiaguang Sun 001 (Math. Comput. Model., 2005)

A Probabilistic Learning Approach for Counterexample Guided Abstraction Refinement. - Fei He 001; Xiaoyu Song; Ming Gu 001; Jia-Guang Sun 001 (ATVA, 2006)

Verifying Java Programs By Theorem Prover HOL. - Anduo Wang; Fei He 001; Ming Gu 001; Xiaoyu Song (COMPSAC (1), 2006)

A combinatorial congestion estimation approach with generalized detours. - Fei He 001; Xiaoyu Song; Ming Gu 001; Lerong Cheng; Guowu Yang; Zhiwei Tang; Jiaguang Sun 001 (Comput. Math. Appl., 2006)

Congestion estimation for hexagonal routing. - Ming Gu 001; Fei He 001; Lerong Cheng; Xiaoyu Song; Guowu Yang (Int. J. Comput. Math., 2006)

Probabilistic optimization for FPGA board level routing problems. - Fei He 001; Xiaoyu Song; Ming Gu 001; Guowu Yang; William N. N. Hung; Jia-Guang Sun 001 (IEEE Trans. Circuits Syst. II Express Briefs, 2006)

Formal Analysis of Publish-Subscribe Systems by Probabilistic Timed Automata. - Fei He 001; Luciano Baresi; Carlo Ghezzi; Paola Spoletini (FORTE, 2007)

Effective heuristics for counterexample-guided abstraction refinement. - Fei He 001; Xiaoyu Song; Ming Gu 001; Jiaguang Sun 001 (ACM Great Lakes Symposium on VLSI, 2007)

A note on "a mapping algorithm for computer-assisted exploration in the design of embedded systems". - Gang Chen 004; Xiaoyu Song; Feng Liu 029; QingPing Tan; Fei He 001 (ACM Trans. Design Autom. Electr. Syst., 2007)

Translation-Based Model Checking for PLC Programs. - Min Zhou 001; Fei He 001; Ming Gu 001; Xiaoyu Song (COMPSAC (1), 2009)

Data mining based decomposition for assume-guarantee reasoning. - He Zhu 001; Fei He 001; William N. N. Hung; Xiaoyu Song; Ming Gu 001 (FMCAD, 2009)

Heuristic-Guided Abstraction Refinement. - Fei He 001; Xiaoyu Song; Ming Gu 001; Jia-Guang Sun 001 (Comput. J., 2009)

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

Comparing Learning Algorithms in Automated Assume-Guarantee Reasoning. - Yu-Fang Chen 001; Edmund M. Clarke; Azadeh Farzan; Fei He 001; Ming-Hsien Tsai 001; Yih-Kuen Tsay; Bow-Yaw Wang; Lei Zhu (ISoLA (1), 2010)

Compositional Abstraction Refinement for Timed Systems. - Fei He 001; He Zhu 001; William N. N. Hung; Xiaoyu Song; Ming Gu 001 (TASE, 2010)

An Analytical Congestion Model with Bounded-Bend Detours. - Fei He 001; Lerong Cheng; Xiaoyu Song; Guowu Yang (J. Circuits Syst. Comput., 2010)

Integrating Evolutionary Computation with Abstraction Refinement for Model Checking. - Fei He 001; Xiaoyu Song; William N. N. Hung; Ming Gu 001; Jiaguang Sun 001 (IEEE Trans. Computers, 2010)

An Efficient Resolution Based Algorithm for SAT. - Min Zhou 001; Fei He 001; Ming Gu 001 (TASE, 2011)

Thread-Modular Model Checking with Iterative Refinement. - Wenrui Meng; Fei He 001; Bow-Yaw Wang; Qiang Liu (NASA Formal Methods, 2012)

Maxterm Covering for Satisfiability. - Liangze Yin; Fei He 001; William N. N. Hung; Xiaoyu Song; Ming Gu 001 (IEEE Trans. Computers, 2012)

VCS: A Verifier for Component-Based Systems. - Fei He 001; Liangze Yin; Bow-Yaw Wang; Lianyi Zhang; Guanyu Mu; Wenrui Meng (ATVA, 2013)

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

Component-Based Modeling and Code Synthesis for Cyclic Programs. - Min Zhou 001; Hai Wan; Chen Su; Liangze Yin; Lianyi Zhang; Fei He 001; Ming Gu 001 (COMPSAC, 2013)

Reusing Search Tree for Incremental SAT Solving of Temporal Induction. - Liangze Yin; Fei He 001; Min Zhou 001; Ming Gu 001 (ICECCS, 2013)

Optimizing the SAT Decision Ordering of Bounded Model Checking by Structural Information. - Liangze Yin; Fei He 001; Ming Gu 001 (TASE, 2013)

A Unified Framework for DPLL(T) + Certificates. - Min Zhou 001; Fei He 001; Bow-Yaw Wang; Ming Gu 001; Jiaguang Sun 001 (J. Appl. Math., 2013)

Clause Replication and Reuse in Incremental Temporal Induction. - Liangze Yin; Fei He 001; Ming Gu 001; Jia-Guang Sun 001 (ICECCS, 2014)

Symbolic assume-guarantee reasoning through BDD learning. - Fei He 001; Bow-Yaw Wang; Liangze Yin; Lei Zhu (ICSE, 2014)

Array Theory of Bounded Elements and its Applications. - Min Zhou 001; Fei He 001; Bow-Yaw Wang; Ming Gu 001; Jiaguang Sun 001 (J. Autom. Reason., 2014)

VeRV: A temporal and data-concerned verification framework for the vehicle bus systems. - Shuo Zhang; Fei He 001; Ming Gu 001 (INFOCOM, 2015)

Leveraging Weighted Automata in Compositional Reasoning about Concurrent Probabilistic Systems. - Fei He 001; Xiaowei Gao; Bow-Yaw Wang; Lijun Zhang 001 (POPL, 2015)

Generalized interface automata with multicast synchronization. - Fei He 001; Xiaoyu Song; Ming Gu 001; Jiaguang Sun 001 (Frontiers Comput. Sci., 2015)

Estimating the Volume of Solution Space for Satisfiability Modulo Linear Real Arithmetic. - Min Zhou 001; Fei He 001; Xiaoyu Song; Shi He; Gangyi Chen; Ming Gu 001 (Theory Comput. Syst., 2015)

Learning-Based Assume-Guarantee Regression Verification. - Fei He 001; Shu Mao; Bow-Yaw Wang (CAV (1), 2016)

Learning Weighted Assumptions for Compositional Verification of Markov Decision Processes. - Fei He 001; Xiaowei Gao; Miaofei Wang; Bow-Yaw Wang; Lijun Zhang 001 (ACM Trans. Softw. Eng. Methodol., 2016)

Assertion Recommendation for Formal Program Verification. - Cong Wang 020; Fei He 001; Xiaoyu Song; Yu Jiang 001; Ming Gu 001; Jiaguang Sun 001 (COMPSAC (1), 2017)

PSpec: a formal specification language for fine-grained control on distributed data analytics. - Chen Luo 002; Fei He 001; Dong Yan; Dan Zhang; Xin Zhou; Bow-Yaw Wang (ICSE (Companion Volume), 2017)

Verification of Implementations of Cryptographic Hash Functions. - Dexi Wang; Yu Jiang 001; Houbing Song; Fei He 001; Ming Gu 001; Jiaguang Sun 001 (IEEE Access, 2017)

Inferring software behavioral models with MapReduce. - Chen Luo 002; Fei He 001; Carlo Ghezzi (Sci. Comput. Program., 2017)

Control flow-guided SMT solving for program verification. - Jianhui Chen; Fei He 001 (ASE, 2018)

When Regression Verification Meets CEGAR. - Fei He 001; Qianshan Yu; Liming Cai (CoRR, 2018)

Efficient software product-line model checking using induction and a SAT solver. - Fei He 001; Yuan Gao; Liangze Yin (Frontiers Comput. Sci., 2018)

SMT-based query tracking for differentially private data analytics systems. - Chen Luo 002; Fei He 001 (Frontiers Comput. Sci., 2018)

Conflict resolution for structured merge via version space algebra. - Fengmin Zhu; Fei He 001 (Proc. ACM Program. Lang., 2018)

Enhancing precision of structured merge by proper tree matching. - Fengmin Zhu; Fei He 001; Qianshan Yu (ICSE (Companion Volume), 2019)

Proving Termination by k-Induction. - Jianhui Chen; Fei He 001 (ASE, 2020)

Proving almost-sure termination by omega-regular decomposition. - Jianhui Chen; Fei He 001 (PLDI, 2020)

Interval counterexamples for loop invariant learning. - Rongchen Xu; Fei He 001; Bow-Yaw Wang (ESEC/SIGSOFT FSE, 2020)

Termination analysis for evolving programs: an incremental approach by reusing certified modules. - Fei He 001; Jitao Han (Proc. ACM Program. Lang., 2020)

Incremental predicate analysis for regression verification. - Qianshan Yu; Fei He 001; Bow-Yaw Wang (Proc. ACM Program. Lang., 2020)

Satisfiability modulo ordering consistency theory for multi-threaded program verification. - Fei He 001; Zhihang Sun; Hongyu Fan (PLDI, 2021)

Automatic Detection and Resolution of Software Merge Conflicts: Are We There Yet? - Bowen Shen; Cihan Xiao; Na Meng 001; Fei He 001 (CoRR, 2021)

PSpec-SQL: Enabling Fine-Grained Control for Distributed Data Analytics. - Chen Luo 002; Fei He 001; Fei Peng; Dong Yan; Dan Zhang; Xin Zhou (IEEE Trans. Dependable Secur. Comput., 2021)

Leveraging Control Flow Knowledge in SMT Solving of Program Verification. - Jianhui Chen; Fei He 001 (ACM Trans. Softw. Eng. Methodol., 2021)

Data-Driven Loop Bound Learning for Termination Analysis. - Rongchen Xu; Jianhui Chen; Fei He 001 (ICSE, 2022)

Interference relation-guided SMT solving for multi-threaded program verification. - Hongyu Fan; Weiting Liu; Fei He 001 (PPoPP, 2022)

EqFix: Fixing LaTeX Equation Errors by Examples. - Fengmin Zhu; Fei He 001 (SETTA, 2022)

Mastery: Shifted-Code-Aware Structured Merging. - Fengmin Zhu; Xingyu Xie; Dongyu Feng; Na Meng 001; Fei He 001 (SETTA, 2022)

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

ProbTA: A sound and complete proof rule for probabilistic verification. - Guanyan Li; Zhilei Han; Fei He 001 (CoRR, 2022)

Lay-it-out: Interactive Design of Layout-Sensitive Grammars. - Fengmin Zhu; Jiangyi Liu; Fei He 001 (CoRR, 2022)

Consistency-preserving propagation for SMT solving of concurrent program verification. - Zhihang Sun; Hongyu Fan; Fei He 001 (Proc. ACM Program. Lang., 2022)

Efficient Summary Reuse for Software Regression Verification. - Fei He 001; Qianshan Yu; Liming Cai (IEEE Trans. Software Eng., 2022)

Data-driven Recurrent Set Learning For Non-termination Analysis. - Zhilei Han; Fei He 001 (ICSE, 2023)

P4b: A Translator from P4 Programs to Boogie. - Chong Ye; Fei He 001 (ESEC/SIGSOFT FSE, 2023)

Satisfiability Modulo Ordering Consistency Theory for SC, TSO, and PSO Memory Models. - Hongyu Fan; Zhihang Sun; Fei He 001 (ACM Trans. Program. Lang. Syst., 2023)

A Characterization Study of Merge Conflicts in Java Projects. - Bowen Shen; Muhammad Ali Gulzar; Fei He 001; Na Meng 001 (ACM Trans. Softw. Eng. Methodol., 2023)

Learning Adaptive Node Embeddings Across Graphs. - Gaoyang Guo; Chaokun Wang; Bencheng Yan; Yunkai Lou; Hao Feng 007; Junchao Zhu; Jun Chen 004; Fei He 001; Philip S. Yu (IEEE Trans. Knowl. Data Eng., 2023)

Automated Ambiguity Detection in Layout-Sensitive Grammars. - Jiangyi Liu; Fengmin Zhu; Fei He 001 (Proc. ACM Program. Lang., 2023)

On the methodology of three-way structured merge in version control systems: Top-down, bottom-up, or both. - Fengmin Zhu; Xingyu Xie; Dongyu Feng; Na Meng 001; Fei He 001 (J. Syst. Archit., 2023)

P4Inv: Inferring Packet Invariants for Verification of Stateful P4 Programs. - Delong Zhang; Chong Ye; Fei He 001 (INFOCOM, 2024)

Leveraging Datapath Propagation in IC3 for Hardware Model Checking. - Hongyu Fan; Fei He 001 (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2024)

Robustness Verification for Checking Crash Consistency of Non-volatile Memory. - Zhilei Han; Fei He 001 (ASPLOS (1), 2025)

On Temporal Verification of Stateful P4 Programs. - Delong Zhang; Chong Ye; Fei He 001 (NSDI, 2025)

Resolving Build Conflicts via Example-Based and Rule-Based Program Transformations. - Sheikh Shadab Towqir; Fei He 001; Todd Mytkowicz; Na Meng 001 (CoRR, 2025)

Structural Abstraction and Refinement for Probabilistic Programs. - Guanyan Li; Juanen Li; Zhilei Han; Peixin Wang; Hongfei Fu 001; Fei He 001 (CoRR, 2025)