We stand with Ukraine

We stand with Ukraine

Hongce Zhang

Orcid: 0000-0003-4001-264X

According to our database¹, Hongce Zhang authored at least 41 papers between 2016 and 2026.

Collaborative distances:

Dijkstra number² of four.
Erdős number³ of four.

Timeline

Legend:

Book In proceedings Article PhD thesis Dataset Other

Links

Online presence:

on orcid.org

On csauthors.net:

Bibliography

2026

AutoINV: Automated Invariant Generation Framework for Formal Verification on High-Level Synthesis Designs.

[DOI]

,

,

,

,

,

CoRR, April, 2026

A-IC3: Learning-Guided Adaptive Inductive Generalization for Hardware Model Checking.

[DOI]

,

,

,

CoRR, April, 2026

IC3-Evolve: Proof-/Witness-Gated Offline LLM-Driven Heuristic Evolution for IC3 Hardware Model Checking.

[DOI]

,

,

,

CoRR, April, 2026

AutoPDR: Circuit-Aware Solver Configuration Prediction for Hardware Model Checking.

[DOI]

,

,

,

,

,

CoRR, March, 2026

LeGend: A Data-Driven Framework for Lemma Generation in Hardware Model Checking.

[DOI]

,

,

,

CoRR, February, 2026

EvolveGen : Algorithmic Level Hardware Model Checking Benchmark Generation through Reinforcement Learning.

[DOI]

,

,

,

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2026

ReVEAL: GNN-Guided Reverse Engineering for Formal Verification of Optimized Multipliers.

[DOI]

,

Daniela Kaufmann

,

,

,

,

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2026

BDD2Seq: Enabling Scalable Reversible-Circuit Synthesis via Graph-to-Sequence Learning.

[DOI]

,

,

,

Proceedings of the Fortieth AAAI Conference on Artificial Intelligence, 2026

2025

Functional Reduction to Speed Up Bounded Model Checking.

[DOI]

,

,

CoRR, December, 2025

SMT-Sweep: Word-Level Representation Unification for Hardware Verification.

[DOI]

,

,

,

,

CoRR, July, 2025

RTLCoder: Fully Open-Source and Efficient LLM-Assisted RTL Code Generation Technique.

[DOI]

,

,

,

,

,

,

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., April, 2025

Transferable Presynthesis PPA Estimation for RTL Designs With Data Augmentation Techniques.

[DOI]

,

,

,

,

,

,

,

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., January, 2025

Hot-FV: A Semi-Formal Test Generation Framework for RTL Functional Coverage Using Warm Starting States.

[DOI]

,

,

,

,

,

Proceedings of the 43rd IEEE International Conference on Computer Design, 2025

Word-Level Counterexample Reduction Methods for Hardware Verification.

[DOI]

,

Proceedings of the Design, Automation & Test in Europe Conference, 2025

NetTAG: A Multimodal RTL-and-Layout-Aligned Netlist Foundation Model via Text-Attributed Graph.

[DOI]

,

,

,

,

,

Proceedings of the 62nd ACM/IEEE Design Automation Conference, 2025

E-morphic: Scalable Equality Saturation for Structural Exploration in Logic Synthesis.

[DOI]

,

,

,

,

Proceedings of the 62nd ACM/IEEE Design Automation Conference, 2025

A Self-Supervised, Pre-Trained, and Cross-Stage-Aligned Circuit Encoder Provides a Foundation for Various Design Tasks.

[DOI]

,

,

,

Proceedings of the 30th Asia and South Pacific Design Automation Conference, 2025

AssertLLM: Generating Hardware Verification Assertions from Design Specifications via Multi-LLMs.

[DOI]

,

,

,

,

,

,

Proceedings of the 30th Asia and South Pacific Design Automation Conference, 2025

2024

AssertLLM: Generating and Evaluating Hardware Verification Assertions from Design Specifications via Multi-LLMs.

[DOI]

,

,

,

,

,

,

CoRR, 2024

Word-Level Augmentation of Formal Proof by Learning from Simulation Traces.

[DOI]

,

Proceedings of the 43rd IEEE/ACM International Conference on Computer-Aided Design, 2024

AsymSAT: Accelerating SAT Solving with Asymmetric Graph-Based Model Prediction.

[DOI]

,

,

,

,

,

Proceedings of the Design, Automation & Test in Europe Conference & Exhibition, 2024

Annotating Slack Directly on Your Verilog: Fine-Grained RTL Timing Evaluation for Early Optimization.

[DOI]

,

,

,

Proceedings of the 61st ACM/IEEE Design Automation Conference, 2024

E-Syn: E-Graph Rewriting with Technology-Aware Cost Functions for Logic Synthesis.

[DOI]

,

,

,

,

,

Proceedings of the 61st ACM/IEEE Design Automation Conference, 2024

DeepIC3: Guiding IC3 Algorithms by Graph Neural Network Clause Prediction.

[DOI]

,

,

,

,

Proceedings of the 29th Asia and South Pacific Design Automation Conference, 2024

2023

r-map: Relating Implementation and Specification in Hardware Refinement Checking.

[DOI]

,

,

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., December, 2023

RTLCoder: Outperforming GPT-3.5 in Design RTL Generation with Our Open-Source Dataset and Lightweight Solution.

[DOI]

,

,

,

,

,

CoRR, 2023

Addressing Variable Dependency in GNN-based SAT Solving.

[DOI]

,

,

,

,

,

CoRR, 2023

WASIM: A Word-level Abstract Symbolic Simulation Framework for Hardware Formal Verification.

[DOI]

,

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023

NeuroPDR: Integrating Neural Networks in the PDR Algorithm for Hardware Model Checking.

[DOI]

,

,

Proceedings of the 5th ACM/IEEE Workshop on Machine Learning for CAD, 2023

MasterRTL: A Pre-Synthesis PPA Estimation Framework for Any RTL Design.

[DOI]

,

,

,

,

,

,

,

Proceedings of the IEEE/ACM International Conference on Computer Aided Design, 2023

INVITED: Generalizing the ISA to the ILA: A Software/Hardware Interface for Accelerator-rich Platforms.

[DOI]

,

,

,

Proceedings of the 60th ACM/IEEE Design Automation Conference, 2023

2021

Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking.

[DOI]

,

,

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2021

Generating Architecture-Level Abstractions from RTL Designs for Processors and Accelerators Part I: Determining Architectural State Variables.

[DOI]

,

,

,

,

Proceedings of the IEEE/ACM International Conference On Computer Aided Design, 2021

Pono: A Flexible and Extensible SMT-Based Model Checker.

[DOI]

,

,

Florian Lonsing

,

,

,

Kristopher Brown

,

,

Clark W. Barrett

Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

2020

Synthesizing Environment Invariants for Modular Hardware Verification.

[DOI]

,

,

Grigory Fedyukovich

,

,

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2020

In Search for a SAT-friendly Binarized Neural Network Architecture.

[DOI]

Nina Narodytska

,

,

,

Proceedings of the 8th International Conference on Learning Representations, 2020

Verification of Recurrent Neural Networks for Cognitive Tasks via Reachability Analysis.

[DOI]

,

,

,

,

,

Nina Narodytska

Proceedings of the ECAI 2020 - 24th European Conference on Artificial Intelligence, 29 August-8 September 2020, Santiago de Compostela, Spain, August 29 - September 8, 2020, 2020

2019

Instruction-Level Abstraction (ILA): A Uniform Specification for System-on-Chip (SoC) Verification.

[DOI]

,

,

Pramod Subramanyan

,

,

,

ACM Trans. Design Autom. Electr. Syst., 2019

ILAng: A Modeling and Verification Platform for SoCs Using Instruction-Level Abstractions.

[DOI]

,

,

,

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

2018

ILA-MCM: Integrating Memory Consistency Models with Instruction-Level Abstractions for Heterogeneous System-on-Chip Verification.

[DOI]

,

Caroline Trippel

,

Yatin A. Manerkar

,

,

Margaret Martonosi

,

Proceedings of the 2018 Formal Methods in Computer Aided Design, 2018

2016

A hardware-based technique for efficient implicit information flow tracking.

[DOI]

,

,

,

,

,

,

Proceedings of the 35th International Conference on Computer-Aided Design, 2016

Loading...