An asynchronous implementation of the maxlist algorithm. - Chris J. Myers; Hao Zheng 001 (ICASSP, 1997)

Architectural Synthesis of Timed Asynchronous Systems. - Brandon M. Bachman; Hao Zheng 001; Chris J. Myers (ICCD, 1999)

Timed circuits: a new paradigm for high-speed design. - Chris J. Myers; Wendy Belluomini; Kip Kallpack; Eric Peskin; Hao Zheng 001 (ASP-DAC, 2001)

Automatic Abstraction for Verification of Timed Circuits and Systems. - Hao Zheng 001; Eric Mercer; Chris J. Myers (CAV, 2001)

Modular verification of timed circuits using automatic abstraction. - Hao Zheng 001; Eric Mercer; Chris J. Myers (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2003)

Characterizing the VCO jitter due to the digital simultaneous switching noise. - Tian Xia; Peilin Song; Hao Zheng 001 (ACM Great Lakes Symposium on VLSI, 2005)

Self-Refereed On-Chip Jitter Measurement Circuit Using Vernier Oscillators. - Tian Xia; Hao Zheng 001; Jing Li; Ahmed Ginawi (ISVLSI, 2005)

Data Dependent Jitter Characterization Based on Fourier Analysis. - Di Mu; Tian Xia; Hao Zheng 001 (DFT, 2006)

Verification of timed circuits with failure-directed abstractions. - Hao Zheng 001; Chris J. Myers; David Walter; Scott Little; Tomohiro Yoneda (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2006)

Timing Jitter Characterization for Mixed-Signal Production Test Using the Interpolation Algorithm. - Tian Xia; Hao Zheng 001 (IEEE Trans. Ind. Electron., 2007)

A Compositional Method With Failure-Preserving Abstraction for Asynchronous Design Verification. - Hao Zheng 001; Jared Ahrens; Tian Xia (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2008)

Synchronization-Based Abstraction Refinement for Modular Verification of Asynchronous Designs. - Hao Zheng 001; Haiqiong Yao; Tomohiro Yoneda (ISVLSI, 2009)

Automated Interface Refinement for Compositional Verification. - Haiqiong Yao; Hao Zheng 001 (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2009)

State space reductions for scalable verification of asynchronous designs. - Haiqiong Yao; Hao Zheng 001; Chris J. Myers (HLDVT, 2010)

Automatic abstraction for verification of cyber-physical systems. - Robert A. Thacker; Kevin R. Jones; Chris J. Myers; Hao Zheng 001 (ICCPS, 2010)

Modular Model Checking of Large Asynchronous Designs with Efficient Abstraction Refinement. - Hao Zheng 001; Haiqiong Yao; Tomohiro Yoneda (IEEE Trans. Computers, 2010)

A Behavioral Analysis Approach for Efficient Partial Order Reduction. - Yingying Zhang; Emmanuel Rodriguez; Hao Zheng 001; Chris J. Myers (HASE, 2011)

Using decision diagrams to compactly represent the state space for explicit model checking. - Hao Zheng 001; Andrew Price; Chris J. Myers (HLDVT, 2012)

Poster Abstract: Methods and Tools for Verification of Cyber-Physical Systems. - Chris J. Myers; Jian Wu; Zhen Zhang 006; Hao Zheng 001; Yingying Zhang (ICCPS, 2012)

An Improvement in Partial Order Reduction Using Behavioral Analysis. - Yingying Zhang; Emmanuel Rodriguez; Hao Zheng 001; Chris J. Myers (ISVLSI, 2012)

A Compositional Minimization Approach for Large Asynchronous Design Verification. - Hao Zheng 001; Emmanuel Rodriguez; Yingying Zhang; Chris J. Myers (SPIN, 2012)

Formal Analysis of a Fault-Tolerant Routing Algorithm for a Network-on-Chip. - Zhen Zhang 006; Wendelin Serwe; Jian Wu; Tomohiro Yoneda; Hao Zheng 001; Chris J. Myers (FMICS, 2014)

Local state space construction for compositional verification of concurrent systems. - Hao Zheng 001 (SPIN, 2014)

Local State Space Analysis Leads to Better Partial Order Reduction. - Hao Zheng 001; Yingying Zhang (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2014)

Compositional Model Checking of Concurrent Systems. - Hao Zheng 001; Zhen Zhang 006; Chris J. Myers; Emmanuel Rodriguez; Yingying Zhang (IEEE Trans. Computers, 2015)

Protocol-guided analysis of post-silicon traces under limited observability. - Hao Zheng 001; Yuting Cao; Sandip Ray; Jin Yang 006 (ISQED, 2016)

An improved fault-tolerant routing algorithm for a Network-on-Chip derived with formal analysis. - Zhen Zhang 006; Wendelin Serwe; Jian Wu; Tomohiro Yoneda; Hao Zheng 001; Chris J. Myers (Sci. Comput. Program., 2016)

POSTER: Towards Precise and Automated Verification of Security Protocols in Coq. - Hernan M. Palombo; Hao Zheng 001; Jay Ligatti (CCS, 2017)

A Post-Silicon Trace Analysis Approach for System-on-Chip Protocol Debug. - Yuting Cao; Hao Zheng 001; Hernan M. Palombo; Sandip Ray; Jin Yang 006 (ICCD, 2017)

Enhancing Observability for Post-Silicon Debug with On-chip Communication Monitors. - Yuting Cao; Hernan M. Palombo; Sandip Ray; Hao Zheng 001 (ISVLSI, 2018)

STAMINA: STochastic Approximate Model-Checker for INfinite-State Analysis. - Thakur Neupane; Chris J. Myers; Curtis Madsen; Hao Zheng 001; Zhen Zhang 006 (CAV (1), 2019)

A Communication-Centric Observability Selection for Post-Silicon System-on-Chip Integration Debug. - Yuting Cao; Hao Zheng 001; Sandip Ray (ISQED, 2019)

Approximation Techniques for Stochastic Analysis of Biological Systems. - Thakur Neupane; Zhen Zhang 006; Curtis Madsen; Hao Zheng 001; Chris J. Myers (CoRR, 2019)

Approximation Techniques for Stochastic Analysis of Biological Systems. - Thakur Neupane; Zhen Zhang 006; Curtis Madsen; Hao Zheng 001; Chris J. Myers (Automated Reasoning for Systems Biology and Medicine, 2019)

Stream-Monitoring Automata. - Hernan M. Palombo; Egor Dolzhenko; Jay Ligatti; Hao Zheng 001 (ICSCA, 2020)

A Distributed Framework for Real Time Object Detection at Low Frame Rates with IoT Edge Nodes. - Lakshmi Kavya Kalyanam; Vishalini Laguduva Ramnath; Srinivas Katkoori; Hao Zheng 001 (iSES, 2020)

Mining Message Flows using Recurrent Neural Networks for System-on-Chip Designs. - Yuting Cao; Parijat Mukherjee; Mahesh Ketkar; Jin Yang 006; Hao Zheng 001 (ISQED, 2020)

Local State Space Analysis to Assist Partial Order Reduction. - Hao Zheng 001; Yingying Zhang; Chris J. Myers (CoRR, 2020)

A Post-Silicon Trace Analysis Approach for System-on-Chip Protocol Debug. - Yuting Cao; Hao Zheng 001; Sandip Ray; Jin Yang 006 (CoRR, 2020)

Model Synthesis for Communication Traces of System Designs. - Hao Zheng 001; Md Rubel Ahmed; Parijat Mukherjee; Mahesh C. Ketkar; Jin Yang 006 (ICCD, 2021)

Mining Message Flows from System-on-Chip Execution Traces. - Md Rubel Ahmed; Hao Zheng 001; Parijat Mukherjee; Mahesh C. Ketkar; Jin Yang 006 (ISQED, 2021)

A Comparative Study of Specification Mining Methods for SoC Communication Traces. - Md Rubel Ahmed; Hao Zheng 001; Parijat Mukherjee; Mahesh C. Ketkar; Jin Yang 006 (ISVLSI, 2021)

Model Synthesis for Communication Traces of System-on-Chip Designs. - Hao Zheng 001; Md Rubel Ahmed; Parijat Mukherjee; Mahesh C. Ketkar; Jin Yang 006 (CoRR, 2021)

Tools and Algorithms for SoC Communication Traces. - Md Rubel Ahmed; Hao Zheng 001 (CoRR, 2021)

Deep Bidirectional Transformers for SoC Flow Specification Mining. - Md Rubel Ahmed; Hao Zheng 001 (CoRR, 2022)

Counterexample Generation for Infinite-State Chemical Reaction Networks. - Mohammad Ahmadi; Zhen Zhang 006; Chris J. Myers; Chris Winstead; Hao Zheng 001 (CoRR, 2022)

Mining SoC Message Flows with Attention Model. - Md Rubel Ahmed; Bardia Nadimi; Hao Zheng 001 (CoRR, 2022)

Mining Patterns From Concurrent Execution Traces. - Md Rubel Ahmed; Hao Zheng 001; Parijat Mukherjee; Mahesh C. Ketkar; Jin Yang 006 (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2022)

System-on-Chip Message Flow Mining with Masked-Language Models. - Md Rubel Ahmed; Bardia Nadimi; Hao Zheng 001 (MWSCAS, 2023)

STAMINA in C++: Modernizing an Infinite-State Probabilistic Model Checker. - Joshua Jeppson; Matthias Volk 001; Bryant Israelsen; Riley Roberts; Andrew Williams; Lukas Buecherl; Chris J. Myers; Hao Zheng 001; Chris Winstead; Zhen Zhang 006 (QEST, 2023)

Rare-Event Guided Analysis of Infinite-State Chemical Reaction Networks. - Mohammad Ahmadi; Lukas Buecherl; Chris J. Myers; Zhen Zhang 006; Chris Winstead; Hao Zheng 001 (QEST+FORMATS, 2024)

A Multi-Expert Large Language Model Architecture for Verilog Code Generation. - Bardia Nadimi; Hao Zheng 001 (CoRR, 2024)

Inferring Message Flows From System Communication Traces. - Bardia Nadimi; Hao Zheng 001 (CoRR, 2024)

PyraNet: A Large Scale Hierarchical Verilog Dataset. - Bardia Nadimi; Ghali Omar Boutaib; Hao Zheng 001 (CoRR, 2024)

AutoModel: Automatic Synthesis of Models From Communication Traces of SoC Designs. - Md Rubel Ahmed; Bardia Nadimi; Hao Zheng 001 (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2024)

AutoFlows: Inferring Message Flows from System Communication Traces. - Bardia Nadimi; Hao Zheng 001 (ISQED, 2025)

VeriMind: Agentic LLM for Automated Verilog Generation with a Novel Evaluation Metric. - Bardia Nadimi; Ghali Omar Boutaib; Hao Zheng 001 (CoRR, 2025)