Prof. Sakallah Honored with Distinguished Alumni Award


Ibrahim N. Hajj (Dean of Engineering and Architecture,
American University of Beirut), left, and Karem Sakallah

Prof. Karem Sakallah was presented with a Distinguished Alumnus Award from the American University of Beirut during the Seventh Faculty of Engineering and Architecture (FEA) Student Conference, May 21-22, 2008.

The award citation reads: To Dr. Karem Sakallah for his contributions to the development of powerful and fast algorithms and their application in the verification of computer hardware designs and software programs.

The following bio and abstract of Prof. Sakallah's plenary talk are taken from the conference program.


Karem Sakallah
BE Electrical Engineering, AUB (1975) MS (1977), PhD (1981) Carnegie Melon University Professor, Department of Electrical Engineering and Computer Science, University of Michigan, Ann Arbor, Michigan, USA

Karem A. Sakallah received the B.E. degree in electrical engineering from the American University of Beirut, Beirut, Lebanon, in 1975, and the M.S.E.E. and Ph.D. degrees in electrical and computer engineering from Carnegie Mellon University, Pittsburgh, PA, in 1977 and 1981, respectively.

In 1981, he was a Visiting Assistant Professor at the Department of Electrical Engineering at Carnegie Mellon University. From 1982 to 1988, he was with the Semiconductor Engineering Computer-Aided Design Group at Digital Equipment Corporation in Hudson, MA, where he headed the Analysis and Simulation Advanced Development Team. Since September 1988, he has been with the University of Michigan, Ann Arbor, as a Professor of Electrical Engineering and Computer Science. He has authored or coauthored more than 200 papers and has presented seminars and tutorials at many professional meetings and various industrial sites. His current research interests include the area of computer-aided design with emphasis on logic and layout synthesis, Boolean satisfiability, discrete optimization, and hardware and software verification.

Since 2006, Dr. Sakallah has been a member of an advisory board for the Qatar Foundation for Education, Science, and Community Development. He is currently on sabbatical leave at Carnegie Mellon University‘s Qatar campus with a mission to help the Qatar Foundation establish Al-Khwarizmi Institute for Computer and Information Science and Engineering.

Dr. Sakallah was an Associate Editor of the IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems from 1995 to 1997 and has served on the program committees of the International Conference on Computer-Aided Design, Design Automation Conference, and the International Conference of Computer Design as well as numerous other workshops. He is currently an Associate Editor of the IEEE Transactions on Computers. He is a fellow of the IEEE and a member of the ACM and Sigma Xi.


From Transistors to Multithreaded Software: An Endless Journey of Discovery

Karem Sakallah
IEEE Fellow and Professor in Electrical Engineering
University of Michigan

Abstract

In this talk I will trace my meandering path from electrical engineering, to computer engineering, to computer science, highlighting some unlikely connections and a few unexpected breakthroughs. The story begins with low-level physics-based modeling of transistors and wires in integrated circuit chips, aimed at predicting circuit behavior and estimating signal timing delays. The first bend in the road occurred when we discovered a hidden Boolean satisfiability (SAT) subproblem within the timing analysis problem. SAT is a fundamental decision problem in computer science and has the distinction of being the first such problem shown to be NP-complete. Undeterred by (or perhaps blissfully ignorant of) this intractability we proceeded to develop a new SAT solver, called GRASP, by building on ideas from the constraint satisfaction field. The key concept in GRASP was the derivation of new facts whenever the solver reached a dead-end in its search for a solution. The particular way in which this was done turned out to be crucial for the scalability of the solver and allowed us to tackle, for the first time, problem instances with tens of thousands of variables and constraints. Since GRASP's debut more than a dozen years ago, literally tens of SAT solvers that are based on its conflict-based learning procedure have been developed by academic and industrial reseachers from around the world, and SAT solvers have become essential tools that are routinely used in many applications. What is perhaps ironic is that the original application that led us to the development of GRASP, namely timing analysis of integrated circuits, turned out not to need all this sophistication after all!

The second unexpected turn in this journey was the realization that much of the complexity in a SAT instance can be attributed to symmetries in its formulation. Borrowing from recentlyproposed ideas for identifying and breaking those symmetries we quickly realized that the dominant tool for symmetry detection would not be able to handle the extremely large SAT instances that had become routine by then. Computationally, symmetry detection is reduced to graph isomorphism whose complexity remains an open question. Against daunting odds, we embarked on the development of an alternative to the nauty package which had been the gold standard for graph automorphism for more than two decades. This required that we delve into abstract algebra and group theory and resulted in the extremely fast and hugely scalable saucy program which can routinely analyze graphs with millions of vertices in seconds.

The latest surprise in this unfolding tale was the rather rapid development of efficient solvers for large systems of mixed constraints, i.e., arbitrary Boolean combinations of predicates from various underlying theories such as the theory of integer linear equalities or the theory of linked lists. A recent crop of so-called satisfiability modulo theory (SMT) solvers integrate "theory solvers" within a backbone SAT solver and achieve remarkable performance and scalability. We are currently exploring the application of SMT solvers for the verification of multi-threaded software running on multi-core chips.