The legacy of Professor Emeritus Edmund Clarke

Turing Award winner and model-checking pioneer Edmund Clarke passed away in December 2020 due to COVID-19. At Carnegie Mellon, Clarke taught courses on model-checking and bug-catching in the School of Computer Science (SCS) and advised many graduate, master’s, and post-doctoral students.

"I have friends who have taken his classes and enjoyed them a great deal," said Charlotte Yano, who served as Clarke's administrative assistant during his time as a professor.

Yano first met Clarke when she was hired by SCS and worked with Clarke's wife, Martha Clarke. She later became Clarke's assistant, finding that he "cared very deeply for his graduate students.” “They were an extension of family, and to a certain degree, his staff like myself were as well. It was very important to him that people feel taken care of and looked out for," Yano said.

Clarke worked with many graduate students throughout his career, one being E. Allen Emerson. Clarke and Emerson wrote a proposal on model-checking, which means running algorithms on models of systems, like communication protocols and circuits, and verifying that the systems work as intended. Their proposal, coupled with the independent work of Joseph Sifakis, earned them the 2007 Turing Award, a prestigious honor in the computing world.

Many of his graduate students, including Will Klieber, stayed at Carnegie Mellon and now work in Carnegie Mellon's Software Engineering Institute (SEI). Klieber wrote his thesis on using Quantified Boolean Formulas (QBF) to check whether a hardware model met its specification.

"He actually was the one who helped me decide to pursue QBF," Klieber said. "I talked to him about the possible topics I could pursue my Ph.D. with and he suggested that, and it turned out to be a really good choice for me. He was a great advisor; he definitely helped me learn the fields and got me to where I could have made sense of some advances in QBF."

Today, Klieber is one of many using model-checking concepts Clarke helped pioneer. At SEI, Klieber is a security researcher, writing programs that detect and fix bugs in software, and much like in Clarke's work, verify that programs work as intended.

"Model-checking is going to be increasingly important for the world, trying to ensure that our software is protected," Klieber said. "What I'm hopeful for is that 10 years down the road, we'll have much better capabilities for verifying software." Klieber added that if he could talk to Clarke again, he'd tell Clarke "how pivotal his work is and to express my gratitude for all that he's done."