Ed Clarke's graduate students stay in close contact with the TuringAward winner, whose educational legacy rivals his research output
By Jennifer Bails
(Wade H. Massie photo)
It was the biggest speech that Edmund Clarke had ever delivered. Last Oct. 20, before the International Conference on Embedded Software in Atlanta, Clarke rose to give his official lecture as a winner of the 2007 A.M. Turing Award.
Recognized as the highest honor in computer science, the $250,000 prize is bestowed annually by the Association for Computing Machinery and is widely considered the Nobel Prize of computing. Clarke shared the honor with a former student, E. Allen Emerson, now at University of Texas at Austin, and Joseph Sifakis of France's National Centre for Scientific Research.
The trio was honored for its efforts to develop an automated method --- called model checking --- to find design errors in computer hardware and software.
Model checking has transformed how the computer industry tests chips, systems and networks, and is increasingly being used to de-bug applications as well, and no one has been at the forefront of its development over the past three decades like Clarke, the FORE Systems university professor of computer science and professor of electrical and computer engineering at Carnegie Mellon.
Yet rather than kicking off his speech by recapping his ground-breaking career, Clarke instead displayed a PowerPoint slide listing over 75 graduate students, post-docs and visitors who worked with him over the past three decades. "They deserve the credit for what I have been able to achieve," he said, with genuine humility. "I attribute my success to all of these people. I often just steered them in the right direction and then tried to keep up."
The sentiment wasn't out of character for a professor as devoted to teaching the next generation of computer scientists as he is to advancing model checking. "Ed has played an important role in model checking, but for me and his other students, he has also 'checked out' to be an important role model," says Bud Mishra (CS'82,'85), professor of computer science, mathematics and cell biology at New York University and one of Clarke's first graduate students at Carnegie Mellon.
Computer scientists used to spend countless hours manually poring over lines of code to hunt for bugs, often in vain. Instead, they now rely on model checking to catch errors in hardware for everything from cell phones to digital memory chips. Fast and automatic, model checking can verify highly sophisticated circuits with as many as 10 to the 120th power configurations. If a design contains an error, model checking will produce a counterexample to help pinpoint the mistake.
The method also is being used to test the reliability of Internet security and privacy protocols, and more recently, to verify that safety-critical software in cars, medical devices and nuclear control systems behave as intended.
Clarke's Turing Award lecture naturally documented his 27-year effort to transform model checking from a theoretical algorithm into an indispensable technology. But his legacy of education is as rich as his legacy of research. His dozens of former graduate students and post-docs have made key contributions in both academia and industry in fields as diverse as systems biology, Internet security and even public policy.
No matter their current interests, they attribute much of their success to the intellectual freedom he afforded them to pursue their own ideas, as they developed the knowledge and skills to become top-notch scientists.
"He gives his students a lot of freedom to pick their problems," says Somesh Jha, associate professor in the Department of Computer Science at University of Wisconsin at Madison. "That was excellent training for when I got out of graduate school and really had to do things on my own."
Clarke says he looks upon his students as equals. "At the same time, I feel like they are my children, and I am sincerely interested in their welfare," he says.
The spirit of collaboration he fosters in this "family" remains very much alive among Clarke's extensive network of graduates, who call each other to share ideas, seek career advice or just to chat. A dozen or so "Ed Clarke alumni" living in the San Francisco Bay area have even organized themselves more formally and gather often. "Every time I am out there, they take me to dinner and talk about their work," Clarke says. "They still seem to really enjoy teaming up with each other." And they all enjoyed the privilege of learning under a legend in computer science.
One member of Ed Clarke's extended family is David L. Dill (CS'82, 87). When he first heard about a nationwide push to replace traditional election ballots with paperless electronic voting machines, he grew uneasy. That's in part because of the lessons he learned as one of Clarke's graduate students at Carnegie Mellon in the early 1980s. There, he helped write a key paper showing that model checking was useful in very-large-scale integration, or VLSI, design, the process of building integrated circuits by combining thousands of transistors on a microprocessor chip.
"I developed a profound respect for the complexity of systems and the incredible difficulty of making them correct --- and the even greater difficulty of making them secure," says Dill, professor of computer science at Stanford University since 1987. "Designers are getting much better at putting bugs in systems than we are at finding them, so that's why my suspicions about electronic voting were immediately raised."
Dill's research has concentrated on the theory and application of model checking and other "formal verification" techniques to system designs. But after the 2000 presidential election debacle, he put some of his science on hold and made a foray into public policy, believing the integrity of American democracy was in jeopardy.
"I got involved in late 2002, early 2003 because states and counties were gearing up for massive purchases of touch-screen machines, and I started wondering why we could trust them," Dill says. He established the lobbying group VerifiedVoting.org and a nonprofit foundation, with the goal of ensuring every vote has a paper record and that voters can verify the accuracy of that record before casting their ballots. So far, the organization and its partners have persuaded 31 states to establish regulations requiring voter-verified paper records --- not just bug-prone computer systems. "Watching the admittedly slow national shift toward better election systems has been really satisfying," Dill says.
Dill views his involvement in political affairs as a natural product of the most lasting insight he gleaned from Clarke. "He taught me that it was possible to use CS theory to solve real problems, and, surprisingly, that I was capable of doing it," Dill says.
Another of Clarke's former collaborators who remains in close contact is Orna Grumberg, who first came to the School of Computer Science from the Technion --- or Israel Institute of Technology --- as a post-doc under Clarke in 1985. Now a full professor in the Technion's computer science department, she returns to Carnegie Mellon each summer as a visiting researcher with Clarke's group.
"Ed always welcomes his visitors warmly and teaches them whatever he knows," says Grumberg, a renowned expert in computer-aided verification of hardware and software. "The atmosphere is one of wonderful collaboration."
Grumberg and Clarke have co-authored dozens of journal articles together, and in 1999, they published the first comprehensive textbook on the theory and practice of model checking. And like Clarke, most of Grumberg's career has been dedicated to solving what is called the state explosion problem in model checking.
Model checking works by expressing the specifications of an abstract model of the hardware or software being analyzed in a special type of notation called temporal logic, which describes how a system will behave over time. Then the model checker reviews every possible state of the model to determine if it is consistent with these specifications.
But as the complexity of a system increases, the number of states to analyze multiplies exponentially, overwhelming the model checker. Finding ways around this conundrum is the key to unlocking all of the inherent power of the method.
"It's a problem we are still fighting, and there is a lot of work left to do," says Grumberg, who in December was named vice dean of the Technion's graduate school. "But there are new inventions and new horizons all the time so I hope that we haven't seen the limits of model checking yet."
Internet security is one of the new frontiers of model checking. Take the security protocols that ensure that credit card information and other personal data are kept confidential when users shop online.
These complex authentication protocols are tough to get right, partly because it is difficult to predict the behavior of potential attackers, says Jha of UW-Madison. Flaws have been identified years after security protocols are released --- much too late, for even small bugs easily can be exploited to cause serious harm, he says.
Jha (CS'96) joined Clarke's group in 1991, earning his PhD and then staying at Carnegie Mellon until 2000 to complete a postdoctoral fellowship. There, he helped develop several improvements to model checking, including one advance that exploited symmetry in hardware design to increase the speed of the technique and another that provided a systematic way to refine the abstract models used.
Now he's drawing on his model checking expertise to make computer networks safer. The method is valuable in the context of security because it exhaustively searches for all possible vulnerabilities. After all, an attacker only needs one door to enter a system and wreak havoc, says Jha, who won the prestigious CAREER award from the National Science Foundation in 2005 to support his work in computer security and privacy.
Recently, Jha co-founded the company NovaShield, which develops technology to detect and eliminate the next generation of malware on personal computers including viruses, worms, trojans, spywares and other threats. Jha says he learned a great deal about "how to be a good scientist" from Clarke and still depends on him for counsel.
Another student who calls Ed Clarke for advice is Mishra, who came to Carnegie Mellon in 1982, the year Clarke left Harvard University to come to Pittsburgh. Along with Dill, he helped write the first paper showing model checking had practical use in hardware verification and wasn't just an academic exercise.
After completing his degree, Mishra searched for applications of his training outside computer science. Today he works at the interface of computing, mathematics and biology as principal investigator for the NYU Bioinformatics Group at the university's Courant Institute of Mathematical Sciences. Founded by Mishra, the group focuses on applying algorithmic, statistical and mathematical models to genomes, cells and populations of cells.
Mishra has developed cutting-edge technologies and statistical analysis tools to attack biological problems that range from deciphering the structure of a genome to understanding chromosomal aberrations and their relation to cancer, malaria, autism, and other diseases.
One of Mishra's innovations --- called optical mapping --- uses fluorescence microscopy to image individual DNA molecules and then produce a map of an organism's genome at low cost compared to conventional sequencing methods. Another can tease apart the genetic contributions people receive from each of their parents, which could help scientists read the genome more accurately and understand evolutionary patterns.
Interestingly, Mishra says, many of his colleagues are beginning to apply the tools of model checking to computational models of biological systems --- a daunting task. "With hardware or software, the engineer gives you the model," he says. "With biology, there is no documentation. If there is an intelligent designer, we didn't get the design."
Mishra said a key lesson he took away from Clarke is that the most beautiful problems to work on are not necessarily the most technically difficult. "I should have realized that when I abandoned model checking and moved on to other things," he says. "But it feels good to be in the wrong." Rather than debugging software, Mishra says, "now I'm interested in debugging humans."
Whether Clarke's students continue to work directly in the field of model checking or move further afield into other disciplines, one thing is certain --- his legacy as an extraordinary teacher and role model will carry on in perpetuity. Last year, a student of a student of a student (who Clarke refers to with amusement as his "great-grand-student") came to host a seminar for one of his classes. And future generations of top computer scientists and leading thinkers will also be able to trace their intellectual roots on a family tree whose lineage begins in his laboratory.
For Clarke, that is perhaps the best aspect of his success, as he imparts his most important advice to those following in his footsteps. "You've got to pick something that you think is an important project and then devote your life to it," he says.
By Jennifer Bails
(Wade H. Massie photo)
It was the biggest speech that Edmund Clarke had ever delivered. Last Oct. 20, before the International Conference on Embedded Software in Atlanta, Clarke rose to give his official lecture as a winner of the 2007 A.M. Turing Award.
Recognized as the highest honor in computer science, the $250,000 prize is bestowed annually by the Association for Computing Machinery and is widely considered the Nobel Prize of computing. Clarke shared the honor with a former student, E. Allen Emerson, now at University of Texas at Austin, and Joseph Sifakis of France's National Centre for Scientific Research.
The trio was honored for its efforts to develop an automated method --- called model checking --- to find design errors in computer hardware and software.
Model checking has transformed how the computer industry tests chips, systems and networks, and is increasingly being used to de-bug applications as well, and no one has been at the forefront of its development over the past three decades like Clarke, the FORE Systems university professor of computer science and professor of electrical and computer engineering at Carnegie Mellon.
Yet rather than kicking off his speech by recapping his ground-breaking career, Clarke instead displayed a PowerPoint slide listing over 75 graduate students, post-docs and visitors who worked with him over the past three decades. "They deserve the credit for what I have been able to achieve," he said, with genuine humility. "I attribute my success to all of these people. I often just steered them in the right direction and then tried to keep up."
The sentiment wasn't out of character for a professor as devoted to teaching the next generation of computer scientists as he is to advancing model checking. "Ed has played an important role in model checking, but for me and his other students, he has also 'checked out' to be an important role model," says Bud Mishra (CS'82,'85), professor of computer science, mathematics and cell biology at New York University and one of Clarke's first graduate students at Carnegie Mellon.
Computer scientists used to spend countless hours manually poring over lines of code to hunt for bugs, often in vain. Instead, they now rely on model checking to catch errors in hardware for everything from cell phones to digital memory chips. Fast and automatic, model checking can verify highly sophisticated circuits with as many as 10 to the 120th power configurations. If a design contains an error, model checking will produce a counterexample to help pinpoint the mistake.
The method also is being used to test the reliability of Internet security and privacy protocols, and more recently, to verify that safety-critical software in cars, medical devices and nuclear control systems behave as intended.
Clarke's Turing Award lecture naturally documented his 27-year effort to transform model checking from a theoretical algorithm into an indispensable technology. But his legacy of education is as rich as his legacy of research. His dozens of former graduate students and post-docs have made key contributions in both academia and industry in fields as diverse as systems biology, Internet security and even public policy.
No matter their current interests, they attribute much of their success to the intellectual freedom he afforded them to pursue their own ideas, as they developed the knowledge and skills to become top-notch scientists.
"He gives his students a lot of freedom to pick their problems," says Somesh Jha, associate professor in the Department of Computer Science at University of Wisconsin at Madison. "That was excellent training for when I got out of graduate school and really had to do things on my own."
Clarke says he looks upon his students as equals. "At the same time, I feel like they are my children, and I am sincerely interested in their welfare," he says.
The spirit of collaboration he fosters in this "family" remains very much alive among Clarke's extensive network of graduates, who call each other to share ideas, seek career advice or just to chat. A dozen or so "Ed Clarke alumni" living in the San Francisco Bay area have even organized themselves more formally and gather often. "Every time I am out there, they take me to dinner and talk about their work," Clarke says. "They still seem to really enjoy teaming up with each other." And they all enjoyed the privilege of learning under a legend in computer science.
One member of Ed Clarke's extended family is David L. Dill (CS'82, 87). When he first heard about a nationwide push to replace traditional election ballots with paperless electronic voting machines, he grew uneasy. That's in part because of the lessons he learned as one of Clarke's graduate students at Carnegie Mellon in the early 1980s. There, he helped write a key paper showing that model checking was useful in very-large-scale integration, or VLSI, design, the process of building integrated circuits by combining thousands of transistors on a microprocessor chip.
"I developed a profound respect for the complexity of systems and the incredible difficulty of making them correct --- and the even greater difficulty of making them secure," says Dill, professor of computer science at Stanford University since 1987. "Designers are getting much better at putting bugs in systems than we are at finding them, so that's why my suspicions about electronic voting were immediately raised."
Dill's research has concentrated on the theory and application of model checking and other "formal verification" techniques to system designs. But after the 2000 presidential election debacle, he put some of his science on hold and made a foray into public policy, believing the integrity of American democracy was in jeopardy.
"I got involved in late 2002, early 2003 because states and counties were gearing up for massive purchases of touch-screen machines, and I started wondering why we could trust them," Dill says. He established the lobbying group VerifiedVoting.org and a nonprofit foundation, with the goal of ensuring every vote has a paper record and that voters can verify the accuracy of that record before casting their ballots. So far, the organization and its partners have persuaded 31 states to establish regulations requiring voter-verified paper records --- not just bug-prone computer systems. "Watching the admittedly slow national shift toward better election systems has been really satisfying," Dill says.
Dill views his involvement in political affairs as a natural product of the most lasting insight he gleaned from Clarke. "He taught me that it was possible to use CS theory to solve real problems, and, surprisingly, that I was capable of doing it," Dill says.
Another of Clarke's former collaborators who remains in close contact is Orna Grumberg, who first came to the School of Computer Science from the Technion --- or Israel Institute of Technology --- as a post-doc under Clarke in 1985. Now a full professor in the Technion's computer science department, she returns to Carnegie Mellon each summer as a visiting researcher with Clarke's group.
"Ed always welcomes his visitors warmly and teaches them whatever he knows," says Grumberg, a renowned expert in computer-aided verification of hardware and software. "The atmosphere is one of wonderful collaboration."
Grumberg and Clarke have co-authored dozens of journal articles together, and in 1999, they published the first comprehensive textbook on the theory and practice of model checking. And like Clarke, most of Grumberg's career has been dedicated to solving what is called the state explosion problem in model checking.
Model checking works by expressing the specifications of an abstract model of the hardware or software being analyzed in a special type of notation called temporal logic, which describes how a system will behave over time. Then the model checker reviews every possible state of the model to determine if it is consistent with these specifications.
But as the complexity of a system increases, the number of states to analyze multiplies exponentially, overwhelming the model checker. Finding ways around this conundrum is the key to unlocking all of the inherent power of the method.
"It's a problem we are still fighting, and there is a lot of work left to do," says Grumberg, who in December was named vice dean of the Technion's graduate school. "But there are new inventions and new horizons all the time so I hope that we haven't seen the limits of model checking yet."
Internet security is one of the new frontiers of model checking. Take the security protocols that ensure that credit card information and other personal data are kept confidential when users shop online.
These complex authentication protocols are tough to get right, partly because it is difficult to predict the behavior of potential attackers, says Jha of UW-Madison. Flaws have been identified years after security protocols are released --- much too late, for even small bugs easily can be exploited to cause serious harm, he says.
Jha (CS'96) joined Clarke's group in 1991, earning his PhD and then staying at Carnegie Mellon until 2000 to complete a postdoctoral fellowship. There, he helped develop several improvements to model checking, including one advance that exploited symmetry in hardware design to increase the speed of the technique and another that provided a systematic way to refine the abstract models used.
Now he's drawing on his model checking expertise to make computer networks safer. The method is valuable in the context of security because it exhaustively searches for all possible vulnerabilities. After all, an attacker only needs one door to enter a system and wreak havoc, says Jha, who won the prestigious CAREER award from the National Science Foundation in 2005 to support his work in computer security and privacy.
Recently, Jha co-founded the company NovaShield, which develops technology to detect and eliminate the next generation of malware on personal computers including viruses, worms, trojans, spywares and other threats. Jha says he learned a great deal about "how to be a good scientist" from Clarke and still depends on him for counsel.
Another student who calls Ed Clarke for advice is Mishra, who came to Carnegie Mellon in 1982, the year Clarke left Harvard University to come to Pittsburgh. Along with Dill, he helped write the first paper showing model checking had practical use in hardware verification and wasn't just an academic exercise.
After completing his degree, Mishra searched for applications of his training outside computer science. Today he works at the interface of computing, mathematics and biology as principal investigator for the NYU Bioinformatics Group at the university's Courant Institute of Mathematical Sciences. Founded by Mishra, the group focuses on applying algorithmic, statistical and mathematical models to genomes, cells and populations of cells.
Mishra has developed cutting-edge technologies and statistical analysis tools to attack biological problems that range from deciphering the structure of a genome to understanding chromosomal aberrations and their relation to cancer, malaria, autism, and other diseases.
One of Mishra's innovations --- called optical mapping --- uses fluorescence microscopy to image individual DNA molecules and then produce a map of an organism's genome at low cost compared to conventional sequencing methods. Another can tease apart the genetic contributions people receive from each of their parents, which could help scientists read the genome more accurately and understand evolutionary patterns.
Interestingly, Mishra says, many of his colleagues are beginning to apply the tools of model checking to computational models of biological systems --- a daunting task. "With hardware or software, the engineer gives you the model," he says. "With biology, there is no documentation. If there is an intelligent designer, we didn't get the design."
Mishra said a key lesson he took away from Clarke is that the most beautiful problems to work on are not necessarily the most technically difficult. "I should have realized that when I abandoned model checking and moved on to other things," he says. "But it feels good to be in the wrong." Rather than debugging software, Mishra says, "now I'm interested in debugging humans."
Whether Clarke's students continue to work directly in the field of model checking or move further afield into other disciplines, one thing is certain --- his legacy as an extraordinary teacher and role model will carry on in perpetuity. Last year, a student of a student of a student (who Clarke refers to with amusement as his "great-grand-student") came to host a seminar for one of his classes. And future generations of top computer scientists and leading thinkers will also be able to trace their intellectual roots on a family tree whose lineage begins in his laboratory.
For Clarke, that is perhaps the best aspect of his success, as he imparts his most important advice to those following in his footsteps. "You've got to pick something that you think is an important project and then devote your life to it," he says.
Image2:
For More Information:
Jason Togyer | 412-268-8721 | jt3y@cs.cmu.edu