The School of Computer Science’s Edmund M. Clarke has led the way for quality assurance processes in the computing industry for more than 30 years. His innovative techniques for automatically verifying the correctness of computer systems are used in transportation, communications and medicine.

The prestigious Franklin Institute recognized Clarke for his work with the Bower Award and Prize for Achievement in Science on Thursday, April 24, in Philadelphia.

A major challenge of modern computer technology and digital electronics is that the scale of today’s systems surpasses people’s capacity to comprehend all of their possible design flaws. When a digital electronic device malfunctions, such as a microprocessor controlling the ailerons of a passenger jet, or an MRI machine being used for a critical medical diagnosis, human lives are at stake.

Since the dawn of computing, engineers have checked for logic errors in computer circuitry or software programs by running simulations to test performance and by manually checking each line of computer code. But as computer chips grew to include hundreds of thousands or millions of transistors, and as software and computer systems similarly grew in complexity, these hit-or-miss "informal verification" methods became inadequate to the task. Errors often went undetected until after a product was released, when correcting even minor errors is expensive.

Model checking, by contrast, is a type of formal verification that analyzes the logic underlying a design, much as a mathematician uses a proof to determine that a theorem is correct. Far from hit-or-miss, model checking considers every possible state of a hardware or software design and determines if it is consistent with the designer's specifications.

Clarke first set the principles and techniques of model checking for finite-state systems in a seminal 1981 paper published with his graduate student, E. Allen Emerson. That paper launched a flood of further research and development of model checking theory and applications, much of it led by Clarke and those who had studied under him. His techniques were adopted by major hardware manufacturers such as IBM, Motorola, Texas Instruments, Intel and Apple.

Clarke joined Carnegie Mellon's Computer Science Department in 1982. In 1995 he became the first recipient of the FORE Systems Professorship, an endowed chair in the School of Computer Science. He was named a University Professor in 2008. He has published nearly 400 papers and other works, including his influential textbook "Model Checking," considered a standard in the field.

Clarke co-founded the conference on Computer Aided Verification and served on its steering committee for many years. He is the former editor-in-chief of Formal Methods in Systems Design. He served on the editorial boards of Distributed Computing, Logic and Computation, and IEEE Transactions in Software Engineering. In 1995 he received a Technical Excellence Award from the Semiconductor Research Corporation. He was a co-recipient of the ACM Kanellakis Award in 1998. In 1999 he received an Allen Newell Award for Excellence in Research from the Carnegie Mellon Computer Science Department.

In 2004 Clarke received the IEEE Harry H. Goode Memorial Award. He was elected to the National Academy of Engineering in 2005 for contributions to the formal verification of hardware and software correctness.

He was a co-recipient of the 2007 ACM Turing Award for his role in developing model checking into a highly effective verification technology, widely adopted in the hardware and software industries. He received the 2008 CADE Herbrand Award for Distinguished Contributions to Automated Reasoning and a 2010 LICS Test-of-Time Award. In 2011 he was elected to the American Academy of Arts and Sciences. He received an honorary doctorate from the Vienna University of Technology in 2012. The Chinese Academy of Sciences awarded him an Einstein Professorship in 2013. Clarke is a fellow of the ACM and the IEEE, and a member of Sigma Xi and Phi Beta Kappa.

In accepting his award, Clarke was joined by fellow Franklin Institute honorees — including CMU's Mark Kryder, co-recipient of the 2014 Benjamin Franklin Medal in Electrical Engineering.

CMU is home to eight Franklin Institute laureates, including President Subra Suresh, who received the 2013 Benjamin Franklin Medal in Mechanical Engineering and Materials Science.