| 2026 | AAAI | BDD2Seq: Enabling Scalable Reversible-Circuit Synthesis via Graph-to-Sequence Learning. | Mingkai Miao, Jianheng Tang, Guangyu Hu, Hongce Zhang |
| 2026 | CAV | Untitled record | Xiaofeng Zhou, Guangyu Hu, Hongce Zhang, Wei Zhang |
| 2026 | DATE | eLogic: An E-Graph-based Logic Rewriting Framework for Majority-Inverter Graphs. | Rongliang Fu, Wei Xuan, Shuo Yin, Guangyu Hu, Chen Chen, Hongce Zhang, Bei Yu, Tsung-Yi Ho |
| 2026 | DATE | FORWORD: Accelerating Formal Datapath Verification via Word-Level Sweeping. | Ziyi Yang, Guangyu Hu, Xiaofeng Zhou, Mingkai Miao, Changyuan Yu, Wei Zhang, Hongce Zhang |
| 2026 | FCCM | AutoINV: Automated Invariant Generation Framework for Formal Verification on High-Level Synthesis Designs. | Xiaofeng Zhou, Linfeng Du, Guangyu Hu, Sharad Sinha, Hongce Zhang, Wei Zhang |
| 2026 | TACAS | ReVEAL: GNN-Guided Reverse Engineering for Formal Verification of Optimized Multipliers. | Chen Chen, Daniela Kaufmann, Chenhui Deng, Zhan Song, Hongce Zhang, Cunxi Yu |
| 2026 | TACAS | EvolveGen : Algorithmic Level Hardware Model Checking Benchmark Generation through Reinforcement Learning. | Guangyu Hu, Xiaofeng Zhou, Wei Zhang, Hongce Zhang |
| 2025 | ASPDAC | AssertLLM: Generating Hardware Verification Assertions from Design Specifications via Multi-LLMs. | Zhiyuan Yan, Wenji Fang, Mengming Li, Min Li, Shang Liu, Zhiyao Xie, Hongce Zhang |
| 2025 | ASPDAC | A Self-Supervised, Pre-Trained, and Cross-Stage-Aligned Circuit Encoder Provides a Foundation for Various Design Tasks. | Wenji Fang, Shang Liu, Hongce Zhang, Zhiyao Xie |
| 2025 | DAC | E-morphic: Scalable Equality Saturation for Structural Exploration in Logic Synthesis. | Chen Chen, Guangyu Hu, Cunxi Yu, Yuzhe Ma, Hongce Zhang |
| 2025 | DAC | NetTAG: A Multimodal RTL-and-Layout-Aligned Netlist Foundation Model via Text-Attributed Graph. | Wenji Fang, Wenkai Li, Shang Liu, Yao Lu, Hongce Zhang, Zhiyao Xie |
| 2025 | DATE | Word-Level Counterexample Reduction Methods for Hardware Verification. | Zhiyuan Yan, Hongce Zhang |
| 2025 | ICCD | Hot-FV: A Semi-Formal Test Generation Framework for RTL Functional Coverage Using Warm Starting States. | Ziyue Zheng, Zhiyuan Yan, Xiangchen Meng, Guangyu Hu, Hongce Zhang, Yangdi Lyu |
| 2024 | ASPDAC | DeepIC3: Guiding IC3 Algorithms by Graph Neural Network Clause Prediction. | Guangyu Hu, Jianheng Tang, Changyuan Yu, Wei Zhang, Hongce Zhang |
| 2024 | DAC | E-Syn: E-Graph Rewriting with Technology-Aware Cost Functions for Logic Synthesis. | Chen Chen, Guangyu Hu, Dongsheng Zuo, Cunxi Yu, Yuzhe Ma, Hongce Zhang |
| 2024 | DAC | Annotating Slack Directly on Your Verilog: Fine-Grained RTL Timing Evaluation for Early Optimization. | Wenji Fang, Shang Liu, Hongce Zhang, Zhiyao Xie |
| 2024 | DATE | AsymSAT: Accelerating SAT Solving with Asymmetric Graph-Based Model Prediction. | Zhiyuan Yan, Min Li, Zhengyuan Shi, Wenjie Zhang, Yingcong Chen, Hongce Zhang |
| 2024 | ICCAD | Word-Level Augmentation of Formal Proof by Learning from Simulation Traces. | Zhiyuan Yan, Hongce Zhang |
| 2023 | DAC | INVITED: Generalizing the ISA to the ILA: A Software/Hardware Interface for Accelerator-rich Platforms. | Bo-Yuan Huang, Hongce Zhang, Aarti Gupta, Sharad Malik |
| 2023 | ICCAD | MasterRTL: A Pre-Synthesis PPA Estimation Framework for Any RTL Design. | Wenji Fang, Yao Lu, Shang Liu, Qijun Zhang, Ceyu Xu, Lisa Wu Wills, Hongce Zhang, Zhiyao Xie |
| 2023 | TACAS | WASIM: A Word-level Abstract Symbolic Simulation Framework for Hardware Formal Verification. | Wenji Fang, Hongce Zhang |
| 2021 | CAV | Pono: A Flexible and Extensible SMT-Based Model Checker. | Makai Mann, Ahmed Irfan, Florian Lonsing, Yahan Yang, Hongce Zhang, Kristopher Brown, Aarti Gupta, Clark W. Barrett |
| 2021 | ICCAD | Generating Architecture-Level Abstractions from RTL Designs for Processors and Accelerators Part I: Determining Architectural State Variables. | Yu Zeng, Bo-Yuan Huang, Hongce Zhang, Aarti Gupta, Sharad Malik |
| 2021 | VMCAI | Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking. | Hongce Zhang, Aarti Gupta, Sharad Malik |
| 2020 | ECAI | Verification of Recurrent Neural Networks for Cognitive Tasks via Reachability Analysis. | Hongce Zhang, Maxwell Shinn, Aarti Gupta, Arie Gurfinkel, Nham Le, Nina Narodytska |
| 2020 | ICLR | In Search for a SAT-friendly Binarized Neural Network Architecture. | Nina Narodytska, Hongce Zhang, Aarti Gupta, Toby Walsh |
| 2020 | VMCAI | Synthesizing Environment Invariants for Modular Hardware Verification. | Hongce Zhang, Weikun Yang, Grigory Fedyukovich, Aarti Gupta, Sharad Malik |
| 2019 | TACAS | ILAng: A Modeling and Verification Platform for SoCs Using Instruction-Level Abstractions. | Bo-Yuan Huang, Hongce Zhang, Aarti Gupta, Sharad Malik |
| 2018 | FMCAD | ILA-MCM: Integrating Memory Consistency Models with Instruction-Level Abstractions for Heterogeneous System-on-Chip Verification. | Hongce Zhang, Caroline Trippel, Yatin A. Manerkar, Aarti Gupta, Margaret Martonosi, Sharad Malik |
| 2016 | ICCAD | A hardware-based technique for efficient implicit information flow tracking. | Jangseop Shin, Hongce Zhang, Jinyong Lee, Ingoo Heo, Yu-Yuan Chen, Ruby B. Lee, Yunheung Paek |