FADI A. ALOUL
C u r r i c u l u m   V i t a e January 1, 2006
PERSONAL	Email Homepage	faloul@aus.edu http://www.aloul.net
EDUCATION	UNIVERSITY of MICHIGAN Doctor of Philosophy in Electrical Engineering and Computer Science (Ph.D.) Graduation: May 2003 Thesis Title: “Scalable Algorithms for Boolean Satisfiability Enabled by Problem Structure” Advisor: Prof. Karem A. Sakallah GPA: 3.82/4.0 UNIVERSITY of MICHIGAN Masters of Electrical Engineering and Computer Science (MSE) Graduation: May 1999 GPA: 3.82/4.0 LAWRENCE TECHNOLOGICAL UNIVERSITY Bachelors of Science in Electrical Engineering (BSEE) Graduation: May 1997 - SUMMA CUM LAUDE GPA: 4.00/4.0
SELECTED COURSES	Operating Systems Computer Networks Distributed Systems Real-Time Computing Communication Networks		Digital Optimization & Synthesis Computer Architecture Digital System Testing Artificial Intelligence Computer Security
PROFESSIONAL EXPERIENCE	Assistant Professor of Computer Engineering, American Univ. of Sharjah Aug 2004- current Visiting Researcher, Advanced Technology Group, Synopsys Summer 2005 Investigated methods of applying satisfiability methods to formal verification. Assistant Professor of Computer Engineering, American Univ. in Dubai Aug 2003- July 2004 Post-Doc Research Fellow, University of Michigan Summer 2003 Responsible for designing and implementing advanced search algorithms. Extended the application of Boolean satisfiability search algorithms to software and hardware verification. Visiting Researcher, Microsoft Research Lab May 2003 Investigated methods of applying incremental satisfiability methods to software verification. Graduate Research Assistant, University of Michigan May 1998 – Apr 2003 Research included the design and evaluation of fast and scalable search algorithms for propositional satisfiability and their deployment in electronic design automation (EDA) applications such as FPGA routing, power leakage reduction, testing, and formal verification of microprocessors and hardware devices. Verification Engineer, Billions of Operations Per Second Inc. (BOPS) Summer 2000 Modeled the instruction set architecture of a VLIW 32-bit DSP core. Developed a new technique using propositional satisfiability to generate instruction sequences that would yield high quality functional test patterns. Implemented the test generator and verified parts of the DSP architecture. United States Patent 20040078674, Billions of Operations Per Second Inc. (BOPS), Mountain View, California, 2004 Graduate Student Instructor, University of Michigan Sep 1997 – Dec 1998 Introduced hardware and software concepts ranging from low level digital logic to high level programming languages (C, C++, and Assembly Language). Prepared lesson plans, conducted lectures, wrote and graded exams, homeworks, and class projects. Managed a team of student instructors.
RESEARCH INTERESTS	Computer-Aided Design Computer and Network Security		Design Automation Optimization
SKILLS	Windows 95/98/2000/NT/XP – Office Linux/HPUX/Solaris Assembly Language Mentor Graphics Design Architect/ IC Station FrameMaker		C/C++ PERL Verilog TCL/TK HTML
PROFESSIONAL SERVICE	Program Committee Member of the ACM/IEEE International Workshop on Logic and Synthesis, IWLS--2003, 2004, 2005, 2006. Program Committee Member of the SIGDA Ph.D. Forum at the Design Automation Conference, DAC--2003, 2004, 2005, 2006, 2007, 2008. Program Committee Member of the International Conference on Theory and Applications of Satisfiability Testing, SAT--2003, 2005. Program Committee Member of the International Symposium on Wireless Systems and Networks, ISWSN--2005. Program Committee Member of the International Workshop on Soft Constraints, CP-SOFT--2003. Session Chair at the International Conference on Modeling, Simulation, and Applied Optimization, ICMSAO--2005.
PROFESSIONAL AFFLIATIONS	Engineering Society of Detroit - President 96-97 IEEE ACM		Tau Beta Pi Eta Kappa Nu Phi Theta Kappa
HONORS	Agere Systems/SRC Graduate Fellowship 01-03 GANN Fellowship 00-01 Design Automation Conference - Ph.D. Forum 00 Graduate Student Research Assistantship 99-01 Graduate Student Teaching Assistantship 97-98 Ranked 1^st among 930 graduating students at LTU		EECS Summer Fellowship 98 LTU Elec. Eng. Excellence Award 97 Lawrence Presidential Scholarship 95-97 Francois J. Castaing Scholarship 95 Dean's List, all terms Ranked 1^st in graduation from highschool
PUBLICATIONS	12 journals, 50+ conference/workshop papers, and 4 technical reports. Electronic versions are available at http://www.aloul.net
PATENTS	F. Aloul and R. Raimi, “Methods and Apparatus for Generating Functional Test Programs by Traversing a Finite State Model of an Instruction Set Architecture,” filed for US patent, Billions of Operations Per Second Inc. (BOPS), Mountain View, California.
INVITED TALKS	I13. Symmetry-Detection and Breaking for Boolean Satisfiability Intel Corporation, Portland, Oregon, July 2005. I12. Symmetry-Detection and Breaking for Boolean Satisfiability Tufts University, Boston, Massachusetts, April 2005. I11. Symmetry Breaking for Pseudo-Boolean Formulas Microsoft Research, Redmond, Washington, December 2003. I10. Scalable Algorithms for Boolean Satisfiability Enabled by Problem Structure Microsoft Research, Redmond, Washington, May 2003. I9. PBS: A Backtrack-Search Pseudo-Boolean Solver and Optimizer University Booth, Design Automation Conference (DAC), Anaheim, California, 2002. I8. Generic ILP versus Specialized 0-1 ILP: An Update IPoCSE Symposium, University of Michigan, 2002. I7. Faster SAT and Smaller BDDs Through Efficient Problem Partitioning GFP Annual Conference, Semiconductor Research Corporation (SRC), Dallas, Texas, 2002. I6. Search-Based SAT Using Zero-Suppressed BDDs University Booth, Design Automation Conference (DAC), New Orleans, Louisiana, 2002. I5. SATIRE – An Incremental SAT Solver University Booth, Design Automation Conference (DAC), Las Vegas, Nevada, 2001. I4. An Experimental Exploration of SAT Problem Hardness IPoCSE Symposium, University of Michigan, 2000. I3. An Exploration of Boolean Satisfiability Solvers and their Application in Hardware Verification 3^rd Ph.D. Forum, Design Automation Conference (DAC), Los Angeles, California, 2000. I2. GRASP – SAT Solver University Booth, Design Automation Conference (DAC), Los Angeles, California, 2000. I1. An Experimental Study of Satisfiability Search Heuristics IPoCSE Symposium, University of Michigan, 1999.
TOOLS	T4. PBS – Incremental pseudo-Boolean backtrack search SAT solver and optimizer. T3. SHATTER – Identifies symmetry-breaking clauses in SAT instances. T2. SATOMETER – Measures progress of backtrack search SAT solvers. T1. MINCE/FORCE – Generates global static variable orderings for SAT and BDDs.
REFERENCES	Available upon request.