the three Turing recipients can be found on page 112.)
Model checking has proven extremely successful at verifying hardware designs. In fact, Xudong Zhao, a graduate student of Clarke’s, showed that model checking could have found Intel’s floating-point division error—and that the company’s fix did indeed correct the problem. Since then, Intel has been a leading user of the technique.
But because even small programs can have millions of different states (a dilemma known to the discipline as the “state explosion problem”), there are limits to the size and complexity of designs that model checking can verify, and it’s been less immediately successful for software. The verification of reactive systems—the combination of hardware and software interacting with an external environment—also remains problematic, due mainly to the difficulty of constructing faithful models.
“We’ve come a long way in the last 28 years, and there’s a huge, huge difference in the scale of problems we can address now as opposed to 1980,” says Holzmann. “But of course we are more ambitious and our applications have gotten more complex, so there is a lot more to be done.”
Other techniques include specialized programming languages and environments that facilitate the creation of reliable, reusable software modules. Eiffel, developed by the Swiss Federal
Institute of Technology’s Bertrand Meyer and recipient of ACM’s 2006 Software System Award, is one well-known example; Alloy, a tool developed by Daniel Jackson and the MIT Software Design Group, has also shown great promise.
To supplement the new languages and techniques, other researchers have focused on outlining more effective procedures and methodologies for developers to follow as they work.
“I’m not a great believer in formal analysis,” says Grady Booch of IBM Research. “Problems tend to appear at this curious intersection of the technological and the social.” After monitoring 50 developers for 24 hours, for example, Booch found that only 30% of their time was spent coding—the rest was spent talking to
news
other members of their team. Avoiding miscommunication, he believes, is therefore critical. Booch is perhaps best known for developing (with Ivar Jacobson and James Rumbaugh) the Unified Markup Language, or UML, a language that uses graphical notations to create an abstract model of a software or hardware system and helps teams communicate, explore, and validate potential designs. More recently, he has continued to focus on the big picture of development with the online Handbook of Software Architecture, which brings together a large collection of software-intensive systems and presents them in a manner that “exposes their essential patterns and that permits comparisons across domains and architectural styles.” The ultimate goal, of course, is to help developers apply that time-tested knowledge to their own programming projects.
“Reuse is easier at a higher level of abstraction,” explains Booch. “So we can reuse patterns, if not necessarily code.”
MIT’s Daniel Jackson is another strong believer in the “big picture” approach. “The first thing we need to do is be honest about the level of reliability that we need,” he asserts. “The second thing is to think about what really cannot go wrong—about what’s mission critical and what’s not.”
Rather than starting with a typical requirements document that outlines
Outstanding Contribution
to ACM Award
Robert A. Walker,
Kent State University
Distinguished Service Award
David A. Patterson, University
of California at Berkeley
Eugene L. Lawler Award for
Humanitarian Contributions
within Computer Science
and Informatics
Randy Wang,
Microsoft Research India
Paris Kanellakis Theory
and Practice Award
Bruno Buchberger,
Johannes Kepler University
Karl V. Karlstrom Outstanding
Educator Award
Randy Pausch,
Carnegie Mellon University
Grace Murray Hopper Award
Vern Paxson, International
Computer Science Institute
and University of California at
Berkeley/Lawrence Berkeley
National Laboratory
A. M. Turing Award
Edmund M. Clarke,
Carnegie Mellon University
E. Allen Emerson,
University of Texas at Austin
Joseph Sifakis, Centre National
de la Recherche Scientifique
and Verimag Laboratory
Software System Award
David Harel, The Weizmann
Institute of Science
Hagi Lachover
Amnon Naamad, EMC Corporation
Amir Pnueli, NYU Courant
Institute of Mathematical Sciences
Michal Politi,
Tadiran Electronic Systems
Rivi Sherman, Negevtech
Mark Trakhtenbrot,
Holon Academic Institute of
Technology and The Open
University of Israel
Aron Trauring, Zotecabv
ACM – Infosys
Foundation Award
Daphne Koller, Stanford University
Doctoral Dissertation Award
Sergey Yekhanin, Princeton University
Honorable Mentions:
Benny Applebaum,
Princeton University
Vincent Conitzer, Duke University
Yan Liu, IBM
ACM- W Athena Lecturer Award
Shafi Goldwasser, MIT and The
Weizmann Institute of Science
ACM – AAAI Allen Newell Award
Leonidas J. Guibas, Stanford University
Several award winners had yet
to be announced at press time.
We’ll have more news about
the 2007 ACM award winners
in next month’s issue.
References:
Archives