Zaher S. Andraus

PhD Candidate - CSE devision

Electrical Engineering and Computer Sciences

University of Michigan - Ann Arbor

2753 CSE Building

2260 Hayward Ave.

Ann Arbor, Michigan 48109-2121

 

Email:

Phone: 734-763-6469

 

Affiliation:

University of Michigan (EECS)

Advanced Computer Architecture Lab (ACAL)

IEEE

GSRC

Technion Alumni

 
Your browser is not Java capable or Java has been disabled.

Research

Publications Tools Awards Groups Miscellaneous Bookmark

 

Publications

Hardware Abstraction and Verification

Reveal: A Formal Verification Tool for Verilog Designs

Zaher S. Andraus, Mark H. Liffiton, and Karem A. Sakallah

To Appear: LPAR 2008, Doha, Qatar.

Scalable Hardware Verification based on Datapath Abstraction, Counterexample-Guided Refinement, and Satisfiability Modulo Theories

Zaher S. Andraus and Karem A. Sakallah

TECHCON 2008, Austin, TX.

Refinement Strategies for Verification Methods Based on Datapath Abstraction

Zaher S. Andraus, Mark H. Liffiton, and Karem A. Sakallah

In Proceedings of Asian and South Pacific Design Automation Conference (ASP-DAC), 2006.

Automatic Abstraction and Verification of Verilog Models (presentation)

Zaher S. Andraus and Karem A. Sakallah

In Proceedings of the 41st Design Automation Conference (DAC) 2004, p. 218-223.

-----

Boolean Satisfiability

A Branch and Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Subformulas

Mark Liffiton, Maher Mneimneh, Ines Lynce, Zaher Andraus, Joao Marques-Silva, and Karem Sakallah

In Constraints Journal.

Advances and Insights Into Parallel SAT Solving

Stephen Plaza, Ian Kountanis, Zaher Andraus, Valeria Bertacco, and Traver Mudge

In Int'l Workshop on Logic and Synthesis (IWLS), 2005.

A Branch and Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Formulas

Maher Mneimneh, Ines Lynce, Zaher Andraus, Joao Marques-Silva and Karem Sakallah

In 8th Int'l Conference on Theory and Applications of Satisfiability Testing (SAT), June 2005.

AMUSE: A Minimally Unsatisfiable Core Extractor (presentation) [Nominated Best Paper Award]

Yoonna Oh, Maher N. Mneimneh, Zaher S. Andraus, Karem A. Sakallah, and Igor L. Markov

 In Proceedings of the 41st Design Automation Conference (DAC) 2004, pp. 518-523.

-----

 

Technical Reports and Conferences w/ no Proceedings

 

CEGAR-Based Formal Hardware Verification: A Case Study

Zaher S. Andraus, Mark H. Liffiton, Karem A. Sakallah

CSE-TR-531-07, May 2007.

Microprocessor Verification Based on Datapath Abstraction and Refinement

Zaher S. Andraus, Mark H. Liffiton, and Karem A. Sakallah

Designing Correct Circuits (DCC 2006), Vienna, Austria, March, 2006.

From Max-SAT to Min-UNSAT: Insights and Applications

Mark H. Liffiton, Zaher S. Andraus, Karem A. Sakallah

CSE-TR-506-05, February 2005.

File Prefetching for Mobile Devices Using On-Line Learning

Zaher Andraus, Anthony Nicholson and Yevgeniy Vorobeychik

 

Tools

Vapor: Verilog Abstraction for Processor Verification

Wave: Word Level Analysis and Validation Engine

Reveal: RTL Efficient Verification via Abstraction to LEUF/CLU(demo)

Amuse: A Minimally Unsatisfiable Core Extractor

MinSat: Satzoo-based Minimally Satisfying Assignment Generator

Awards and Recognitions

3rd Annual CSE Honors Competition (University of Michigan), 2006: 2nd Place

 

AMUSE: A Minimally Unsatisfiable Core Extractor

Yoonna Oh, Maher Mneimneh, Zaher S. Andraus, Karem A. Sakallah and Igor L. Margov

Nominated Best Paper Award in DAC 2004.

CADathlon 2004: Third Place.

Technion, 1998: Excellence Award for highest GPA amongst Technion applicants.

2nd place in "Mathematics' Activities Competition" in Israel, 1995.

Groups

S-Team

PSAT

SWERVE

Personal Flavor