Edmund M. Clarke (1945–2020)

Edmund Melson Clarke, Jr., a celebrated American academic who developed methods for mathematically proving the correctness of computer systems, died on December 22, 2020 at the age of 75 from complications of COVID-19. Clarke was awarded the A.M Turing Award in 2008 with his former student E. Allen Emerson and the French computer scientist Joseph Sifakis, for their work on model checking.

"I've never liked to fly, although I've done my share of it. I wanted to do something that would make systems like airplanes safer," Clarke said in a 2014 video produced by the Franklin Institute when he was awarded their 2014 Bower Award and Prize for Achievement in Science^a "For 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."

Model checking is a practical approach for machine verification of mathematical models of hardware, software, communications protocols, and other complex computing systems. The technique is used to formally validate all of the states that a system can possibly reach, even when the number of states seems impossibly large—for example, more than the number of stars in the universe. These techniques, first developed when he was an assistant professor at Harvard University in 1981, are now widely used in the design of computing hardware and safety-critical systems and are increasingly being used for protocol validation and computer security.

Clarke grew up in rural Virginia and was the first person in his family to graduate from college. He earned a bachelor's degree in mathematics in 1967 at the University of Virginia, a master's degree in mathematics the following year at Duke University, and a Ph.D. in computer science from Cornell in 1976. He then returned to Duke where he taught for two years before becoming an assistant professor at Harvard University in 1978. He joined CMU's faculty in 1982, was appointed full professor in 1989, University Professor in 2008, and became an Emeritus Professor in 2015.

As Clarke explained in the 2008 Turing Award Paper,¹ "Model checkers typically have three main components: (1) a specification language, based on propositional temporal logic. (2) a way of encoding a state machine representing the system to be verified, and (3) a verification procedure, that uses an intelligent exhaustive search of the state space to determine if the specification is true or not." Most model checkers, upon finding that the specification is violated, provide the counterexample, which is invaluable in debugging complex systems.

His students remember Clarke for the way that he mentored them both professionally and personally. For instance, Somesh Jha, now a professor at the University of Wisconsin reminisced "Ed treated his students like family. Martha and Ed regularly invited students and their families to their house. I remember those parties quite fondly."

"He used to insist that we should work on important problems of practical significance, but at the same time, he also had appreciation of basic research on foundational problems," said A. Prasad Sistla, one of Clarke's students at Harvard who followed him to CMU and now a professor of Computer Science at the University of Illinois at Chicago.

"Ed was a perfect mentor for me," recalls ACM Fellow David Dill, now an Emeritus Professor at Stanford, known for his work in formal verification and the security of electronic voting systems. "He only gave positive reinforcement. He would ask questions, refer to related work that would be useful to know, suggest directions and research topics, and carefully follow my presentations … Once I started listening, I suddenly became productive."

"On his 69^th birthday, 100 of his students, postdocs, and visitors from all over the world gathered together in Pittsburgh to celebrate his planned retirement and to praise his enormous contribution to the Model Checking area. He was surrounded with love and appreciation," recalls ACM Fellow Orna Grumberg, a professor of computer science at Technion in Israel.

---

"Ed was a perfect mentor for me. He only gave positive reinforcement. He would ask questions, refer to related work that would be useful to know, suggest directions and research topics, and carefully follow my presentations … Once I started listening, I suddenly became productive." ACM FELLOW DAVID DILL EMERITUS PROFESSOR, STANFORD UNIVERSITY

---

Some of his colleagues also noted Clarke's mentoring. Randal Bryant mentioned it first when asked for recollection. "He always had a group of graduate students and post-docs who collaborated with him and with each other very effectively. He launched them into very successful careers in both industry and academia." Bryant also noted the scope of Clarke's lifelong work: hardware to software to protocols—"He was intellectually broad and open-minded."

Indeed, academia was the family business, with Clarke's wife Martha serving as the graduate admissions co-ordinator for the CMU Computer Science Department and the School of Computer Science, where she worked for 28 years until her retirement in 2014. The two were high-school sweethearts, marrying immediately after they graduated. They celebrated their 52nd anniversary in 2020.

Clarke's son, Jonathan, said that he gave his three sons a "joy of learning" and encouraged them to take courses in science and mathematics. Jonathan earned a Ph.D. in Finance and is now a professor and senior associate dean at Georgia Tech's Business School. His younger brother, Jeffrey, earned a medical degree and is an oncologist and assistant professor at Duke University School of Medicine. Their older brother, James, earned a Ph.D. in Chemistry and is the Director of Quantum Hardware at Intel in Portland, Oregon. In addition to his wife and sons, Clarke is also survived by six grandchildren.

His wife Martha reflected on Clarke's own joy of learning, "He was always reading. I remember him even taking scientific papers to read during high school football games." His interests were wider than simply academics, with members of his family noting his fondness for fishing, photography, and flying kites.

A founder of the Computer Aided Verification Conference in 1989, Clarke was also the former editor-in-chief of the Springer journal Formal Methods in Systems Design. He was a Fellow of the ACM and the IEEE, and a member of both Sigma Xi and Phi Beta Kappa. He was inducted into the National Academy of Engineering in 2005, and the American Academy of Arts and Sciences in 2011.

Clarke was the co-recipient of the 1998 ACM Paris Kanellakis Theory and Practice Award, CMU's 1999 Allen Newell Award for Excellence in Research, the 2004 IEEE Harry H. Goode Memorial Award, and the Conference on Automated Deduction's 2008 Herbrand Award for Distinguished Contributions to Automated Reasoning.