In Memoriam: E. Allen Emerson

E. Allen Emerson was the first graduate student of Edmund M. Clarke at Harvard University. After discussing several ideas for Allen’s dissertation, they identified a promising candidate: verifying a finite-state system against a formal specification. According to Martha Clarke, Edmund’s widow, it was during a walk across Harvard Yard that they decided to call it “model checking.” Emerson received his Ph.D. in applied mathematics for this work in 1981. Twenty-five years later, he and Clarke (along with Joseph Sifakis) shared the ACM A.M. Turing Award in 2007 for this and related work.

Ernest Allen Emerson II passed away on October 15, 2024. He was born in Dallas, Texas, on June 2, 1954, to Ernest and Ina Lee Emerson. He graduated first in his high school class, where he learned programming on GE Mark I and Burroughs computers. He next attended the University of Texas at Austin (UT Austin). While there, he developed a lifelong interest in formal methods of computation. As noted in the biography accompanying his Turing Award citation, he was partly inspired by reading “Proof of a Program: FIND,”³ a Communications paper by 1980 Turing Award recipient Tony Hoare, and by a talk by Zohar Manna on fixpoints and the Tarski-Knaster Theorem.

After obtaining his B.S. in mathematics in 1976, Emerson enrolled at Harvard for graduate study. Upon receiving his Ph.D., Emerson joined the computer science faculty at UT Austin.

Also on the faculty of UT Austin was Edsger Dijkstra, who believed that programmers should reason about the correctness of their programs and not rely on mechanical program checkers. In other words, Dijkstra was no fan of model checking. In 1985, Dijkstra analyzed a short paper Emerson published at the ACM Symposium on Programming Languages¹ as part of his Tuesday Afternoon Club.

“Dijkstra took extreme umbrage to the paper, and he wrote a scathing memo criticizing me harshly,” recalled Emerson in his 2019 oral history.⁶ “It was devastating.”

“But to Dijkstra’s surprise, I returned the next week with a memo of my own, defending myself and counterattacking,” with an argument that Dijkstra accepted. The two became close friends, with Emerson concluding that Dijkstra eventually conceded his argument regarding the benefits of model checking, telling him: “Sir, you are at risk of winning the argument.”

Emerson retired in 2016 as Regents Chair and professor of Computer Science, entering emeritus status.

The Turing Award citation states, “For their role in developing model checking into a highly effective verification technology that is widely adopted in the hardware and software industries.” In addition, Emerson made significant contributions to temporal logic and introduced the concept of computation tree logic (CTL and CTL*), all of which are used in verifying concurrent and real-time systems, communications protocols, and microprocessors.

Emerson advised many notable Ph.D. students. One of them, Thomas Wahl (GrammaTech, Inc.), recounted, “[he was] …high entropy-high reward in most interactions. The learning curve was steep (tough for a student spoiled with strictly organized lectures, homework, and exams).” Another former student, Charanjit Jutla (Simons Institute, UC Berkeley), noted: “He was a logician at heart, following on the traditions of Alonzo Church to whom Allen could trace his academic legacy.” Kedar Namjoshi (Nokia Bell Labs) recalls, “We’d meet to discuss research, but the conversation would soon diverge into science fiction (we both loved it; he was a particular fan of Larry Niven’s Ringworld); rabbits (he had two as pets); and every other topic under the sun.” He went on to state, “He made getting a Ph.D. so enjoyable that I would happily have done it all over again. He held us all to his own exacting standards, but he did so with gentleness, patience, trust, and humor”—a sentiment that several of his other former advisees echoed.

Emerson received other honors for his work, including the 1998 ACM Paris Kanellakis Theory and Practice Award (joint with Randal Bryant, Edmund M. Clarke, and Kenneth L. McMillan for the development of symbolic model checking, He also received the 1999 CMU Newell Research Excellence Award and the IEEE’s 2006 Test of Time Award.

Emerson met his future wife, Leisa, at the public schools they attended in Dallas. They married in 1977. He is survived by his wife, his sister, and a niece and nephew and their families. His obituary notes Emerson’s love of travel, books, family, and work.^1,4,5,7