winners of the Turing Award 2007
We copy from the web page:
http://www.acm.org/press-room/news-releases/turing-award-07/
ACM Turing Award Honors Founders of Automatic Verification Technology
Researchers Created Model Checking Technique for Hardware and Software
Designers
acm
The Association for Computing Machinery
Advancing Computing as a Science & Profession
Contact: Virginia Gold
212-626-0505
vg...@acm.org
NEW YORK, February 4, 2008 - ACM, the Association for Computing
Machinery, has named Edmund M. Clarke, E. Allen Emerson, and Joseph
Sifakis the winners of the 2007 A.M. Turing Award, widely considered
the most prestigious award in computing, for their original and
continuing research in a quality assurance process known as Model
Checking. Their innovations transformed this approach from a
theoretical technique to a highly effective verification technology
that enables computer hardware and software engineers to find errors
efficiently in complex system designs. This transformation has
resulted in increased assurance that the systems perform as intended
by the designers. The Turing Award, named for British mathematician
Alan M. Turing, carries a $250,000 prize, with financial support
provided by Intel Corporation and Google Inc. Clarke of Carnegie
Mellon University, and Emerson of the University of Texas at Austin,
working together, and Sifakis, working independently for the Centre
National de la Recherche Scientifique at the University of Grenoble in
France, developed this fully automated approach that is now the most
widely used verification method in the hardware and software
industries.
ACM President Stuart Feldman said the work of Clarke, Emerson and
Sifakis has had a major impact on designers and manufacturers of
semiconductor chips. "These industries face a technology explosion in
which products of unprecedented complexity have to operate as expected
for companies to survive. This verification advance enabled these
industries to shorten time to market and increase product integrity.
Without the conceptual breakthrough pioneered by these researchers, we
might still be stuck with chips that have many errors and would lack
the power and speed of today's equipment. This is a great example of
an industry-transforming technology arising from highly theoretical
research," Feldman said.
Model Checking as a standard procedure for quality assurance has
enabled designers and manufacturers to address verification problems
that span both hardware and software. It has also helped them to gain
mathematical confidence that complex computer systems meet their
specifications, and it has provided added security for a range of both
common and critical computing applications.
"Intel and the entire computing industry have been direct
beneficiaries of the awardees' ground-breaking work," said Andrew
Chien, Vice President in the Corporate Technology Group and Director
of Research of Intel Corporation. "Our researchers and engineers have
worked closely with Clarke, Emerson, and Sifakis for 15 years.
Insights from their novel automatic verification results have been
widely adopted by the entire industry. These Model Checking approaches
provide dramatically better coverage when searching for design
errors."
"Google, like any contemporary technology company, owes a great deal
of its success to the work of pioneering researchers who have come
before," said Alan Eustace, Senior Vice President of Engineering at
Google. "We are proud to honor the award winners for their innovative
solution to a difficult and pervasive issue and we hope this will
encourage and inspire those who now face the technology challenges of
the future."
Migrating from Pure Research to Industrial Reality
Logical errors in digital circuit designs, software, and communication
protocols are an important problem for system designers. They often
result in delays in getting new products to market, failures of
critical systems already in use, and expensive replacement of faulty
hardware and patching of flawed software.
Model Checking started as an academic research idea. The continuing
research of Clarke, Emerson, and Sifakis as well as others in the
international research community over the last 27 years led to the
creation of new logics, as well as new algorithms and surprising
theoretical results. This in turn has stimulated the creation of many
Model Checking tools by both academic and industrial teams, resulting
in the widespread industrial use of Model Checking.
Many major hardware and software companies now rely heavily on Model
Checking. Common examples include verification of the designs for
integrated circuits such as microprocessors, as well as communication
protocols, software device drivers, real-time embedded systems, and
security algorithms.
Among the beneficiaries of Model Checking are personal computer users,
medical device makers, and nuclear power plant operators. As
computerized systems pervade daily life, consumers rely on digital
controllers to supervise critical functions of cars, airplanes, and
industrial plants. Digital switching technology has replaced analog
components in the telecommunications industry, and security protocols
enable e-commerce applications and privacy. Wherever significant
investments or human lives are at risk, quality assurance for the
underlying hardware and software components becomes paramount.
Background
In 1981, Edmund Clarke and Allen Emerson working in the U.S., and
Joseph Sifakis working independently in France with J.P. Queille,
authored seminal papers that founded what has become the highly
successful field of Model Checking. This verification technology
offers two advantages. It provides an algorithmic means of determining
whether an abstract model, such as a hardware or software design,
satisfies a formal specification, such as a temporal logic formula
(i.e., a pattern for a sequence of events). In addition, it identifies
the counter-examples that show the source of the problem, which must
be addressed should the stated property specification not hold.
A drawback of the Model Checking approach, known as the state-
explosion problem, seemed to limit its applicability to small designs
of mainly academic interest. Randal Bryant, Edmund Clarke, Allen
Emerson and Kenneth McMillan invented Symbolic Model Checking, which
greatly extended the size and complexity of systems that could be
verified. It also led to the widespread adoption of Model Checking by
the computer hardware industry. For this invention, Bryant, Clarke,
Emerson, and McMillan received the 1998 Paris Kanellakis Award for
Theory and Practice from ACM. In 1999, they also received the Allen
Newell Award for Research Excellence from Carnegie Mellon University.
Sifakis, together with Thomas A. Henzinger and Sergio Yovine, extended
the Model Checking approach to address verification of real time
systems. In 2001, Sifakis received the Centre National de la Recherche
Scientifique Silver Medal.
Edmund M. Clarke
Dr. Clarke is the FORE Systems Professor of Computer Science and
Professor of Electrical and Computer Engineering at Carnegie Mellon
University. He has served on the editorial boards of numerous journals
and is the former editor-in-chief of Formal Methods in Systems Design.
He is a co-founder with Robert Kurshan, Amir Pnueli, and Joseph
Sifakis of the International Conference on Computer Aided Verification
(CAV) and serves on the steering committee. He received a Technical
Excellence Award from the Semiconductor Research Corporation in 1995,
and the IEEE Harry M. Goode Memorial Award in 2004. He is a Fellow of
ACM and the IEEE Computer Society, and was elected to the National
Academy of Engineering in 2005. Dr. Clarke was awarded a B.A. degree
in mathematics from the University of Virginia and a M.A. degree in
mathematics from Duke University. He earned a Ph.D. degree in computer
science from Cornell University, and has taught at Duke University and
Harvard University.
E. Allen Emerson
Dr. Emerson is an Endowed Professor in Computer Sciences at the
University of Texas at Austin. He was a co-recipient of the 2006 Test-
of-Time Award from the IEEE Symposium on Logic in Computer Science
(LICS) for his research on efficient Model Checking in the
propositional mu-calculus, a highly expressive temporal logic, with
Chin-Laung Lei. He has served on the editorial boards of several
leading journals in applied logic and formal methods, including ACM
Transactions on Computational Logic, Formal Aspects of Computing, and
Formal Methods in Systems Design. He serves on the steering committee
of the International Symposium on Automated Technology for
Verification and Analysis (ATVA) as well as the International
Conference on Verification, Model Checking, and Abstract
Interpretation (VMCAI). Dr. Emerson received a B.S. degree in
mathematics from University of Texas at Austin, and a Ph.D. in applied
mathematics from Harvard University.
Joseph Sifakis
Dr. Sifakis is the founder of Verimag Laboratory, a leading research
center for embedded systems in Grenoble, France, where he was director
from 1993-2006. He is Research Director of Centre National de la
Recherche Scientifique, and Director of the CARNOT Institute on
Intelligent Software and Systems in Grenoble. Dr. Sifakis is a member
of the editorial board of several journals, and the scientific
coordinator of the Artist2 and ArtistDesign European Networks of
Excellence on Embedded Systems Design. He is co-founder with Edmund
Clarke, Robert Kurshan, and Amir Pnueli of the International
Conference on Computer Aided Verification (CAV). He earned a degree in
electrical engineering from the Technical University of Athens and a
Ph.D. in computer science from the University of Grenoble.
ACM will present the Turing Award at the annual ACM Awards Banquet on
June 21, 2008, in San Francisco, CA.
About the A.M. Turing Award
The A.M. Turing Award was named for Alan M. Turing, the British
mathematician who articulated the mathematical foundation and limits
of computing, and who was a key contributor to the Allied
cryptanalysis of the German Enigma cipher during World War II. Since
its inception in 1966, the Turing Award has honored the computer
scientists and engineers who created the systems and underlying
theoretical foundations that have propelled the information technology
industry. For additional information, click on http://awards.acm.org/turing.
About ACM
ACM (www.acm.org) is widely recognized as the premier organization for
computing professionals, delivering resources that advance the
computing and IT disciplines, enable professional development, and
promote policies and research that benefit society. ACM hosts the
computing industry's leading Digital Library and Portal to Computing
Literature, and serves its global membership with journals and
magazines, special interest groups, conferences, workshops, electronic
forums, Career Resource Centre and Professional Development Centre.
See:
http://www.acm.org/press-room/news-releases/turing-award-07/
No comments:
Post a Comment