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)

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

Boolean Ring Satisfiability. - Nachum Dershowitz; Jieh Hsiang; Guan-Shieng Huang; Daher Kaiss (SAT, 2004)

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

Seqver : A Sequential Equivalence Verifier for Hardware Designs . - Daher Kaiss; Silvian Goldenberg; Zurab Khasidashvili (ICCD, 2006)

Boolean Rings for Intersection-Based Satisfiability. - Nachum Dershowitz; Jieh Hsiang; Guan-Shieng Huang; Daher Kaiss (LPAR, 2006)

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

A compositional theory for post-reboot observational equivalence checking of hardware. - Zurab Khasidashvili; Daher Kaiss; Doron Bustan (FMCAD, 2009)

Post-silicon timing diagnosis made simple using formal technology. - Daher Kaiss; Jonathan Kalechstain (FMCAD, 2014)