PITTSBURGH—The Franklin Institute in Philadelphia has named Edmund M. Clarke, the FORE Systems University Professor of Computer Science and professor of electrical and computer engineering, as the recipient of the 2014 Bower Award and Prize for Achievement in Science.

He is one of two Carnegie Mellon University professors that The Franklin Institute is honoring as leaders in science, engineering, technology and business. Mark H. Kryder, University Professor of Electrical and Computer Engineering, is the recipient of the 2014 Benjamin Franklin Medal in Electrical Engineering.

“Mark Kryder and Edmund Clarke have each made distinctive and important contributions to information technology in our time, and they have each had a transformative impact on the way computer hardware, software, and systems are designed and developed. Carnegie Mellon is very proud that two of the university’s outstanding faculty members are being honored in the same year by an institution with the global stature of The Franklin Institute,” said CMU President Subra Suresh, who received the 2013 Benjamin Franklin Medal in Mechanical Engineering and Materials Science.

The awards program, founded in 1824, is one way The Franklin Institute preserves Benjamin Franklin’s legacy. It recognizes individuals whose great innovation has benefited humanity, advanced science, launched new fields of inquiry and deepened understanding of the universe. Alexander Graham Bell, Thomas Edison, Albert Einstein and Jane Goodall are among The Franklin Institute’s laureates.

Edmund M. Clarke

Clarke’s Bower Prize recognizes “his leading role in the conception and development of techniques for automatically verifying the correctness of a broad array of computer systems, including those found in transportation, communications and medicine.”

These techniques, known as Model Checking, analyze the logic underlying a design, much as a mathematician uses a proof to determine that a theorem is correct. The automated method for identifying design errors considers every possible state of a hardware or software design and determines if it is consistent with the designer’s specifications. Clarke implemented the first Model Checker in 1982, the same year he joined CMU’s faculty.

Randal E. Bryant, dean of the School of Computer Science, noted that The Franklin Institute this year had solicited nominations for the Bower Prize for “individuals who have made significant scientific contributions to the verification and validation of computer systems in hardware and/or software.”

“In my mind, this is a perfect summary of Ed Clarke’s career,” Bryant said.  Working with a number of graduate students and postdoctoral researchers, he laid the theoretical foundations for Model Checking, created algorithms that can perform Model Checking on large-scale hardware and software systems, and demonstrated many of its applications.  We are proud that he has done much of this work as a member of the CMU faculty.”

The Bower Award and Prize includes a gold medal and a cash prize of $250,000. It was established in 1988 with a bequest from Henry Bower, a Philadelphia chemical manufacturer who also endowed an award for business leadership. Takeo Kanade, the U.A. and Helen Whitaker University Professor of Computer Science and Robotics, received the 2008 Bower Award and Prize.

Clarke directs Computational Modeling and Analysis of Complex Systems, a National Science Foundation project that is extending Model Checking and other formal verification techniques to produce insights into a variety of complex systems, from embedded computer systems to cancer.

He previously won the Association for Computing Machinery’s (ACM) A.M. Turing Award, often referred to as the “Nobel Prize of computing,” with E. Allen Emerson of the University of Texas at Austin and Joseph Sifakis of the University of Grenoble in France, for their pioneering work on Model Checking. He also received the ACM’s Paris Kanellakis Theory and Practice Award and CMU’s School of Computer Science (SCS) Allen Newell Award for Research Excellence with Emerson, Bryant and SCS alumnus Kenneth L. McMillan, now with Microsoft Research, for their invention of Symbolic Model Checking.

Clarke has received numerous individual honors and awards from industry and academic organizations. He is a fellow of the ACM and the Institute of Electrical and Electronic Engineers (IEEE), and an elected member of the National Academy of Engineering (NAE) and American Academy of Arts and Sciences. The Chinese Academy of Sciences this year named him an Einstein Professor. He co-founded the International Conference on Computer-Aided Verification and is the former editor-in-chief of Formal Methods in Systems Design.

Mark H. Kryder

Kryder is being recognized along with Shunichi Iwasaki of Japan’s Tohoku Institute of Technology “for the development and realization of the system of Perpendicular Magnetic Recording, which has enabled a dramatic increase in the storage capacity of computer-readable media.”

Kryder and Iwasaki are receiving one of six Benjamin Franklin Medals awarded in 2014. Other medal winners are being recognized for leadership in chemistry, earth and environmental science, life science, mechanical engineering and physics. John R. Anderson, Richard King Mellon University Professor of Psychology and Computer Science, won the 2011 Benjamin Franklin Medal in Computer and Cognitive Science.

Kryder joined CMU’s faculty in 1978 and founded the university’s Magnetics Technology and Data Storage Systems centers (DSSC) in 1983 and 1990, respectively. Under his direction, the DSSC became the world’s largest academic research center in the field of data storage technology.

From 1998 to 2007, he was senior vice president of research and chief technical officer at Seagate Technology. During this time, Seagate introduced perpendicular recording technology and full disk encryption, both of which are used on hard disk drives today. He also initiated the company’s program on Heat Assisted Magnetic Recording (HAMR), which Seagate recently announced was used to demonstrate an information storage density of one terabit per square inch. Upon retiring from Seagate in 2007, he returned to CMU to continue research on HAMR and to initiate a research program on materials for spin torque transfer random access memory (STTRAM).

Kryder has published more than 370 papers and holds 24 patents in the field of magnetic memory and storage technology. He is an elected member of the NAE and a fellow of the American Physical Society and the IEEE, which has bestowed three awards upon him. Kryder’s other honors include the American Institute of Physics’ George E. Pake Prize and the Public Service Medal of Singapore.

Clarke, Kryder and fellow honorees will receive their awards at a ceremony and dinner on April 24, 2014, in Philadelphia. It culminates a weeklong series of events and activities that connect laureates with students and the community. While celebrating the “Franklins” of today, The Franklin Institute hopes to inspire and influence the innovation of the “Franklins” of tomorrow.