CLEVER: Divide and Conquer Combinational Logic Equivalence VERification with False Negative Elimination. - John Moondanos; Carl-Johan H. Seger; Ziyad Hanna; Daher Kaiss (CAV, 2001)

An enhanced cut-points algorithm in formal equivalence verification. - Zurab Khasidashvili; John Moondanos; Daher Kaiss; Ziyad Hanna (HLDVT, 2001)

A proof engine approach to solving combinational design automation problems. - Gunnar Andersson; Per Bjesse; Byron Cook; Ziyad Hanna (DAC, 2002)

TRANS: efficient sequential verification of loop-free circuits. - Zurab Khasidashvili; John Moondanos; Ziyad Hanna (HLDVT, 2002)

Alignability equivalence of synchronous sequential circuits. - Amnon Rosenmann; Ziyad Hanna (HLDVT, 2002)

High capacity and automatic functional extraction tool for industrial VLSI circuit designs. - Sasha Novakovsky; Shy Shyman; Ziyad Hanna (ICCAD, 2002)

A signal correlation guided ATPG solver and its applications for solving difficult industrial cases. - Feng Lu 002; Li-C. Wang; Kwang-Ting Cheng; John Moondanos; Ziyad Hanna (DAC, 2003)

SAT-based methods for sequential hardware equivalence verification without synchronization. - Zurab Khasidashvili; Ziyad Hanna (BMC@CAV, 2003)

Design automation with mixtures of proof strategies for propositional logic. - Gunnar Andersson; Per Bjesse; Byron Cook; Ziyad Hanna (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2003)

Theoretical framework for compositional sequential hardware equivalence verification in presence of design constraints. - Zurab Khasidashvili; Marcelo Skaba; Daher Kaiss; Ziyad Hanna (ICCAD, 2004)

Parallel Multithreaded Satisfiability Solver: Design and Implementation. - Yulik Feldman; Nachum Dershowitz; Ziyad Hanna (PDMC, 2004)

A Signal Correlation Guided Circuit-SAT Solver. - Feng Lu 002; Li-C. Wang; Kwang-Ting (Tim) Cheng; John Moondanos; Ziyad Hanna (J. Univers. Comput. Sci., 2004)

Space-Efficient Bounded Model Checking. - Jacob Katz; Ziyad Hanna; Nachum Dershowitz (DATE, 2005)

Simultaneous SAT-Based Model Checking of Safety Properties. - Zurab Khasidashvili; Alexander Nadel; Amit Palti; Ziyad Hanna (Haifa Verification Conference, 2005)

Bounded Model Checking with QBF. - Nachum Dershowitz; Ziyad Hanna; Jacob Katz (SAT, 2005)

A Clause-Based Heuristic for SAT Solvers. - Nachum Dershowitz; Ziyad Hanna; Alexander Nadel (SAT, 2005)

Encoding RTL Constructs for MathSAT: a Preliminary Report. - Marco Bozzano; Roberto Bruttomesso; Alessandro Cimatti; Anders Franzén; Ziyad Hanna; Zurab Khasidashvili; Amit Palti; Roberto Sebastiani (PDPAR@CAV, 2005)

Generation of shorter sequences for high resolution error diagnosis using sequential SAT. - Sung-Jui (Song-Ra) Pan; Kwang-Ting Cheng; John Moondanos; Ziyad Hanna (ASP-DAC, 2006)

Post-reboot Equivalence and Compositional Verification of Hardware. - Zurab Khasidashvili; Marcelo Skaba; Daher Kaiss; Ziyad Hanna (FMCAD, 2006)

A Scalable Algorithm for Minimal Unsatisfiable Core Extraction. - Nachum Dershowitz; Ziyad Hanna; Alexander Nadel (SAT, 2006)

An Efficient Diagnostic Test Pattern Generation Framework Using Boolean Satisfiability. - Feijun Zheng; Kwang-Ting Cheng; Xiaolang Yan; John Moondanos; Ziyad Hanna (ATS, 2007)

A Lazy and Layered SMT($ mathcal{BV}$) Solver for Hard Industrial Verification Problems. - Roberto Bruttomesso; Alessandro Cimatti; Anders Franzén; Alberto Griggio; Ziyad Hanna; Alexander Nadel; Amit Palti; Roberto Sebastiani (CAV, 2007)

Abstract Modeling and Formal Verification of Microprocessors. - Ziyad Hanna (CSR, 2007)

Industrial Strength SAT-based Alignability Algorithm for Hardware Equivalence Verification. - Daher Kaiss; Marcelo Skaba; Ziyad Hanna; Zurab Khasidashvili (FMCAD, 2007)

Towards a Better Understanding of the Functionality of a Conflict-Driven SAT Solver. - Nachum Dershowitz; Ziyad Hanna; Alexander Nadel (SAT, 2007)

A symbolic execution framework for algorithm-level modelling. - Ziyad Hanna; Thomas F. Melham (HLDVT, 2009)

A symbolic execution framework for algorithm-level modelling and verification of computer microarchitecture. - Ziyad Hanna (2011)

Formal Analysis of Security Data Paths in RTL Design. - Jamil Mazzawi; Ziyad Hanna (Haifa Verification Conference, 2012)

Challenging problems in industrial formal verification. - Ziyad Hanna (FMCAD, 2014)

Democratization of Formal Verification with Collective Intelligence. - Ziyad Hanna (FMCAD, 2015)