Distinguishing Characteristics

Carnegie Mellon is known worldwide for our broad vision of computer science. We act quickly to explore new directions. We are fearless in pushing the frontiers of our field. Computer Science at Carnegie Mellon is also distinctive for our research style, our educational programs, our success at diversity, our culture, and our organizational structure. It is the union of all these features, rather than any one of them, that truly distinguishes us.

What Distinguishes Us

First and foremost, we value the quality and impact of our research. Our research style is to strive simultaneously for high quality and high impact.

• We do highly collaborative and interdisciplinary work. Our collaborations cross between the Computer Science Department (CSD), other units in SCS and on campus, other universities, and industry—as witnessed by our many joint grants, centers, laboratories, and institutes, and by our many joint faculty appointments. In hiring, we ask “Whom might this person work with?” In allocating offices, we mix faculty and students in different research areas to be on the same floor or in the same office. But more subtly, our interdisciplinary style crosses traditional boundaries within computer science, often labeled “AI,” “Systems,” and “Theory.” Pick almost any one of our faculty members and he or she will say “I do both AI and Theory” or “I do both Systems and Theory” or “I do all three!” Our ability not just to cross disciplines but also to cross research styles makes us stand out.
• We build things. We have a long-standing history of building real systems for real users with real-world impact. Synergistically, we use scientific methods to build things and we develop new scientific methods based on what we learn from building.
• We think big. We are willing to take risks in our individual research agendas, to support uncommon research areas, to start uncharted research areas, and to dream of projects beyond what a single faculty member could accomplish on his or her own. Thinking big and doing big requires teamwork, thereby reinforcing our collaborative style.

Second, we show leadership in education.

• We designed our Ph.D. program with the goal of preparing our students to be leaders in academia and industry. We abide by the principle “Research from Day One.” We revamped the core course structure of the Ph.D. program to retain rigor but allow flexibility. We initiated the Speakers Club, a formal writing requirement, and a TA evaluation process. Other SCS Ph.D. programs have been modeled after ours. We closely evaluate and monitor our Ph.D. students through our once unique “Black Friday” which many of our competitors (e.g., MIT, UC Berkeley, Harvard, and University of Pennsylvania) and other Carnegie Mellon units (e.g., ECE) have adopted. B-1
• Over the past decade, our enthusiasm for and dedication to the undergraduate program have increased tremendously. We now offer a challenging and unique curriculum, attracting top applicants internationally. We have a devoted faculty who have won the University advising award (James Roberts andMark Stehlik) and the University teaching award (Steven Rudich).
• Three years ago, we started an elite Fifth-Year Master’s Program for our own top undergraduates.
• Our educational program reflects our expanding universe model (see below).

Third, we have a supportive culture that brings out the best in people.

• Despite our large size, we live by the Reasonable Person Principle. This principle implies interacting at a level of mutual trust and support beyond just assuming that others around us will behave reasonably.
• We take collective responsibility for our students and faculty. Black Friday provides shared faculty oversight over individual advisor/advisee relationships. The January SCS teaching meeting provides an open sanity check on the distributed, but shared process by which we do teaching assignments.
• We presume success. When we admit students to our Ph.D. program, we expect them to finish. When we hire a new junior faculty member we expect him or her to be promoted through the ranks. To meet these expectations–while upholding our high standards–we work hard to provide the supportive environment needed. We started a faculty mentoring process last year, we run an Immigration Course and more recently an Emigration Course for our students, and we share a computing facilities support staff. Our “presume success” model has deep-seated implications from the way we structure our Ph.D. program to the way senior faculty look after junior faculty.

Fourth, we have dramatically increased the number of female undergraduates in computer science.

• The percentage of women out of all students receiving undergraduate degrees in computer science at Carnegie Mellon now hovers around 33%, almost twice the national percentage.
• The Women@SCS organization has broken the traditional gender divide and created an activist and welcoming computing community.

Finally, we have an unusual organizational structure.

• Our model of CSD is an expanding universe. With respect to the rest of the School of Computer Science (SCS), CSD is the stable home for traditional areas of computer science and the nurturing home to seed new, emerging areas. Indeed, the other units of SCS have “spun out” from CSD, creating their own subdisciplines or interdisciplines of computer science.
• The lack of rigid administrative or structural boundaries within SCS gives us agility, nimbleness, and true collegiality. Whereas other schools often have an adversarial relationship between the dean and department heads, our ability to work as one in SCS means a lack of turf battles.

Only at Carnegie Mellon: An Example Success Story

In 1981 Ed Clarke and Al Emerson, and also independently, J.P. Queille and Joseph Sifakis, invented temporal logic model checking. In this approach specifications are expressed in a temporal logic and systems are modeled as finite state transition systems. In 1982 Clarke joined the faculty at Carnegie Mellon from Harvard.

In 1984, Randy Bryant joined Carnegie Mellon from CalTech. He had just invented a new data structure, ordered binary decision diagrams (BDDs), while working in the area of symbolic verification of circuits. BDDs are an efficient representation of boolean functions. His 1986 paper on BDDs has the highest citation count of any publication in the Citeseer database.

In 1987, Ken McMillan entered the Ph.D. program in Computer Science. During the CSD Immigration Course (IC), he heard Clarke talk about model checking and Bryant talk about BDDs. He wondered if BDDs could be applied to model checking. The rest is history. Initial conversations with both Clarke and Bryant were polite but not excessively encouraging. McMillan took it upon himself to show how to use BDDs to represent states and state transitions of a system and to represent the temporal logic specification of its properties. This symbolic representation of the key ingredients in model checking enabled an efficient search over the state space. In 1990 Clarke and four of his students, including McMillan, published a paper entitled “Symbolic Model Checking: 1020 States and Beyond.” Up until the use of BDDs, model checkers at the time could handle only 104 to 105 states. McMillan received the 1992 ACM Dissertation Award for his Ph.D. thesis research and has continued to work in verification ever since.

Hardware companies picked up model checking technology, especially after the 1994 Intel Pentium disaster, when Clarke sent his graduate student Xudong Zhao to Intel to show how model checking could be used to verify the fix. Now, most major hardware companies use model checking along with simulation to validate their designs. Model checking has also received the attention of software companies. Microsoft uses model checking to help debug device driver code, a major source of errors in the Windows operating system. The Microsoft Static Driver Verifier ships with the Windows Driver Development Kit, and thus a model checker is on every driver developer’s workstation in Microsoft and available to third-party device driver writers. Bill Gates mentioned this work in his 2002 OOPSLA keynote address.

In 1997, the ACM awarded Bryant, Clarke, Emerson, and McMillan the Kanellakis Theory and Practice Award to recognize the importance of their fundamental work and its practical impact. This multi-decade experience reinforces some of our core beliefs:

• Hire talented people.
• Admit great graduate students.
• The IC is invaluable. (You might find your thesis topic on your first day of graduate school.)
• Persistence pays. (Model checking will celebrate its 25th birthday next year.)

Computer Science Department
Carnegie Mellon University, Pittsburgh PA 15213-3891
Wean Hall 4212. Phone: 412-268-2565, Fax: 412-268-5576