| 2015 | FMCAD | Democratization of Formal Verification with Collective Intelligence. | Ziyad Hanna |
| 2014 | FMCAD | Challenging problems in industrial formal verification. | Ziyad Hanna |
| 2007 | CAV | A Lazy and Layered SMT($\mathcal{BV}$) Solver for Hard Industrial Verification Problems. | Roberto Bruttomesso, Alessandro Cimatti, Anders Franzn, Alberto Griggio, Ziyad Hanna, Alexander Nadel, Amit Palti, Roberto Sebastiani |
| 2007 | CSR | Abstract Modeling and Formal Verification of Microprocessors. | Ziyad Hanna |
| 2007 | FMCAD | Industrial Strength SAT-based Alignability Algorithm for Hardware Equivalence Verification. | Daher Kaiss, Marcelo Skaba, Ziyad Hanna, Zurab Khasidashvili |
| 2007 | SAT | Towards a Better Understanding of the Functionality of a Conflict-Driven SAT Solver. | Nachum Dershowitz, Ziyad Hanna, Alexander Nadel |
| 2006 | ASPDAC | Generation of shorter sequences for high resolution error diagnosis using sequential SAT. | Sung-Jui (Song-Ra) Pan, Kwang-Ting Cheng, John Moondanos, Ziyad Hanna |
| 2006 | FMCAD | Post-reboot Equivalence and Compositional Verification of Hardware. | Zurab Khasidashvili, Marcelo Skaba, Daher Kaiss, Ziyad Hanna |
| 2006 | SAT | A Scalable Algorithm for Minimal Unsatisfiable Core Extraction. | Nachum Dershowitz, Ziyad Hanna, Alexander Nadel |
| 2005 | DATE | Space-Efficient Bounded Model Checking. | Jacob Katz, Ziyad Hanna, Nachum Dershowitz |
| 2005 | SAT | Bounded Model Checking with QBF. | Nachum Dershowitz, Ziyad Hanna, Jacob Katz |
| 2005 | SAT | A Clause-Based Heuristic for SAT Solvers. | Nachum Dershowitz, Ziyad Hanna, Alexander Nadel |
| 2004 | ICCAD | Theoretical framework for compositional sequential hardware equivalence verification in presence of design constraints. | Zurab Khasidashvili, Marcelo Skaba, Daher Kaiss, Ziyad Hanna |
| 2003 | DAC | A signal correlation guided ATPG solver and its applications for solving difficult industrial cases. | Feng Lu, Li-C. Wang, Kwang-Ting Cheng, John Moondanos, Ziyad Hanna |
| 2002 | DAC | A proof engine approach to solving combinational design automation problems. | Gunnar Andersson, Per Bjesse, Byron Cook, Ziyad Hanna |
| 2002 | ICCAD | High capacity and automatic functional extraction tool for industrial VLSI circuit designs. | Sasha Novakovsky, Shy Shyman, Ziyad Hanna |
| 2001 | CAV | CLEVER: Divide and Conquer Combinational Logic Equivalence VERification with False Negative Elimination. | John Moondanos, Carl-Johan H. Seger, Ziyad Hanna, Daher Kaiss |