2014 Bower Award Goes To… Validation

The Franklin Institute has recognized the work of Edmund Clarke, FORE Systems University Professor of Computer Science at Carnegie Mellon University, with the Bower Award and Prize for Achievement in Science, for his "leading role in the conception and development of techniques for automatically verifying the correctness of a broad array of computer systems."

The general topic cluster for this year’s Bower Science Award was Computer and Cognitive Science. (The overall topic is drawn from a rotating selection that also includes Chemistry, Civil and Mechanical Engineering, Earth and Environmental Science, Electrical Engineering, Life Science, and Physics.) With the overall cluster determined, the Institute’s Committee on Science and the Arts develops three topics for presentation to a Theme Selection Committee, which in turn chooses the specific topic for the award.

Jeremy Johnson, a computer science professor at Drexel University, serves on the Committee on Science and the Arts, and also as part of the computer and cognitive science cluster, helps select the award recipients. Johnson proposed the theme of verification and validation and championed it to the Selection Committee. According to Johnson, "I chose the topic because of the importance of computers for running the infrastructure of the modern world and the difficulty and importance of making sure they run correctly." He focused on formal methods of verification, he says, because "I believe there is great potential for formal methods, and the time is ripe to see them better utilized in the development of computer systems." He also felt that granting a Bower Award in the field would give the methods more exposure and help them realize their potential.

Rajeev Alur, Zisman Family Professor in the Department of Computer and Information Science at the University of Pennsylvania, agrees about the importance of work in verification and validation. "The motivation for this field is to make sure that systems work correctly," he says. "These days, every engineered product has some software running inside it. An example would be the software that’s running inside a pacemaker. But software comes with a challenge, which is that it may be buggy, and failure could lead to catastrophic loss or life-threatening situations. It could also be very expensive. The goal of verification is to make sure at design time that you are sure the software works as intended, so the errors don’t crop up while the systems are actually running."

Randal Bryant, professor of computer science and Dean of the School of Computer Science at Carnegie Mellon University, concurs. "This is an area that’s not the mainstream, most-known part of computer science. It’s not the World Wide Web or something like that. But the field does have some serious substance behind it, and it’s also had some real impact on industry." According to Alur, research into verification has proceeded slowly but steadily, and has reached the point where it can be applied to real-world systems. "It’s very good for the field and it’s a nice recognition that this is an important technology. We’re very happy that the Institute chose this field," says Alur.

The Institute’s Theme Selection Committee ended up being convinced by Johnson’s argument, and chose verification and validation as the topic for the award. (The other contenders were parallel processing and computer translation of natural language.) With the topic chosen, the next step was to define it and solicit nominations, for which the Institute enlisted Alur’s help. "When they chose verification as one of the topics, they contacted me because of my work in the area, and they wanted to make sure that the description in the call for nominations covered as many subareas as possible, and that the topic was construed as broadly as possible," he says. The final description, as posted on the Institute’s Call for Nominations page, read, "Research areas include but are not limited to: formal specification, formal semantics, model checking, automated theorem proving, static analysis and type checking, proof checking, and program derivation."

Alur also made sure the call for nominations was advertised to relevant scientific mailing lists. His efforts paid off, he says: "We got an excellent slate of nominees, from the U.S. but also from international sources. And in lots of different sub-areas."

The eventual winner, Edmund Clarke, calls his approach to verification "model checking," an approach he has been focusing on for more than 30 years. In model checking, systems specifications are expressed in a propositional temporal logic, and a search procedure determines whether the specifications are satisfied. This approach is more efficient and requires less manual intervention than the more common simulation method and, according to Clarke, has become widely adopted for verifying hardware and is beginning to be used to verify software as well.

Clarke received the 2007 ACM Turing Award together with E. Allen Emerson and Joseph Sifakis for their role in developing model checking. Says Bryant, "If you’re going to pick someone in this field, here’s the guy."

Logan Kugler is a freelance technology writer based in Silicon Valley. He has written for over 60 major publications.