Microprocessor Simulation and Program Assembling Using Spreadsheets. - Ali El-Hajj; Karim Y. Kabalan; Maher N. Mneimneh; Feras Karablieh (Simul., 2000)

Scalable Hybrid Verification of Complex Microprocessors. - Maher N. Mneimneh; Fadi A. Aloul; Christopher T. Weaver; Saugata Chatterjee; Karem A. Sakallah; Todd M. Austin (DAC, 2001)

Search-Based SAT Using Zero-Suppressed BDDs. - Fadi A. Aloul; Maher N. Mneimneh; Karem A. Sakallah (DATE, 2002)

ZBDD-Based Backtrack Search SAT Solver. - Fadi A. Aloul; Maher N. Mneimneh; Karem A. Sakallah (IWLS, 2002)

SAT-based sequential depth computation. - Maher N. Mneimneh; Karem A. Sakallah (ASP-DAC, 2003)

Computing Vertex Eccentricity in Exponentially Large Graphs: QBF Formulation and Solution. - Maher N. Mneimneh; Karem A. Sakallah (SAT, 2003)

Preserving synchronizing sequences of sequential circuits after retiming. - Maher N. Mneimneh; Karem A. Sakallah; John Moondanos (ASP-DAC, 2004)

AMUSE: a minimally-unsatisfiable subformula extractor. - Yoonna Oh; Maher N. Mneimneh; Zaher S. Andraus; Karem A. Sakallah; Igor L. Markov (DAC, 2004)

A Branch-and-Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Formulas. - Maher N. Mneimneh; Inês Lynce; Zaher S. Andraus; João Marques-Silva 001; Karem A. Sakallah (SAT, 2005)

Principles of Sequential-Equivalence Verification. - Maher N. Mneimneh; Karem A. Sakallah (IEEE Des. Test Comput., 2005)

Structure-driven algorithms for equivalence verification and infeasibility checking. - Maher N. Mneimneh (2006)

A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas. - Mark H. Liffiton; Maher N. Mneimneh; Inês Lynce; Zaher S. Andraus; João Marques-Silva 001; Karem A. Sakallah (Constraints An Int. J., 2009)

A spreadsheet tool for antenna design. - Karim Y. Kabalan; Ali El-Hajj; Mohammed Al-Husseini; Maher N. Mneimneh (Comput. Appl. Eng. Educ., 2011)