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
“how can you ever
hope to build a
dependable system
if you don’t know
what ‘dependable’
means?” asks mit’s
Daniel Jackson.
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
Awards
2007 ACM Award Winners
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.
