Guangyu (Gary) Hu

Guangyu (Gary) Hu

Researcher at Huawei Hong Kong Research Center, Fermat Lab

Huawei Hong Kong Research Center, Fermat Lab

About Me

Hello! Thank you for visiting my page. I am a researcher at Huawei Hong Kong Research Center, Fermat Lab, working on LLM + formal verification reasoning and hardware formal verification. I received my Ph.D. in IIP-MICS (Microelectronics) from HKUST in 2025, supervised by Prof.Hongce Zhang and Prof.Wei Zhang. I graduated from Xiamen University in February 2021.

See my resume here.

Interests
  • Formal Verification
  • Hardware Security
  • Invariant Synthesis
  • Model Checking
  • Deep Learning
Education

  • Ph.D. in IIP-MICS (Microelectronics), Feb. 2022 - 2025

    The Hong Kong university of Science and Technology

  • B.Eng. in Software Engineering, Sep. 2016 - Feb. 2021

    Xiamen University

Selected Publications

Mingkai Miao, Guangyu Hu, Ziyi Yang, Hongce Zhang (2026). IC3-Evolve: Proof-/Witness-Gated Offline LLM-Driven Heuristic Evolution for IC3 Hardware Model Checking. IJCAI.

PDF Code

Xiaofeng Zhou, Guangyu Hu, Hongce Zhang, Wei Zhang (2026). A-IC3: Learning-Guided Adaptive Inductive Generalization for Hardware Model Checking. CAV.

PDF Code DOI Artifact (Zenodo)

Mingkai Miao, Guangyu Hu, Wei Zhang, Hongce Zhang (2026). LeGend: A Data-Driven Framework for Lemma Generation in Hardware Model Checking. DAC.

PDF Code

Guangyu Hu, Chen Chen, Xiaofeng Zhou, Jiaxi Zhang, Wei Zhang, Hongce Zhang (2026). AutoPDR: Circuit-Aware Solver Configuration Prediction for Hardware Model Checking. ISEDA.

PDF Code

Da Chen, Guangyu Hu, Kaihong Xu, Kaichao Liang, Songjiang Li, Wei Yang, Xiangyu Wen, Mingxuan Yuan (2026). SegSEM: Enabling and Enhancing SAM2 for SEM Contour Extraction. ISCAS.

PDF DOI

Guangyu Hu, Xiaofeng Zhou, Wei Zhang, Hongce Zhang (2026). EvolveGen: Algorithmic Level Hardware Model Checking Benchmark Generation through Reinforcement Learning. TACAS.

PDF Code DOI

Mingkai Miao, Jianheng Tang, Guangyu Hu, Hongce Zhang (2026). BDD2Seq: Enabling Scalable Reversible-Circuit Synthesis via Graph-to-Sequence Learning. AAAI.

PDF Code DOI

Chen Chen, Guangyu Hu, Cunxi Yu, Yuzhe Ma, Hongce Zhang (2025). E-morphic: Scalable Equality Saturation for Structural Exploration in Logic Synthesis. DAC.

PDF Code DOI

Chen Chen, Guangyu Hu, Dongsheng Zuo, Cunxi Yu, Yuzhe Ma, Hongce Zhang (2024). E-Syn: E-Graph Rewriting with Technology-Aware Cost Functions for Logic Synthesis. DAC.

PDF Code DOI

Guangyu Hu, Jianheng Tang, Changyuan Yu, Wei Zhang, Hongce Zhang (2024). DeepIC3: Guiding IC3 Algorithms by Graph Neural Network Clause Prediction. ASP-DAC.

Code DOI

Guangyu Hu, Wei Zhang, Hongce Zhang (2023). NeuroPDR: Integrating Neural Networks in the PDR Algorithm for Hardware Model Checking. MLCAD.

Code DOI

See all publications

Services

Conference Technical Program Committee

  • International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI) 2027
  • International Symposium of EDA (ISEDA) 2026

Artifact Evaluation Committee

  • Computer-Aided Verification (CAV) 2025
  • Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2025
  • Object-Oriented Programming, Systems, Languages & Applications (OOPSLA) 2025
  • USENIX Conference on File and Storage Technologies (FAST) 2024
  • Integrated Formal Methods (iFM) 2024, 2025

Sub-Reviewer & Student Reviewer

  • Design Automation Conference (DAC) 2026
  • Asia and South Pacific Design Automation Conference (ASP-DAC) 2025
  • Formal Methods in Computer-Aided Design (FMCAD) 2024

Benchmark Contribution

  • Hardware Model Checking Competition (HWMCC) 2024, 2025 — benchmark contributor (submission)

Contact