(Image Credit: UT Austin)
E. Allen Emerson, an early-day supporter of the CAV conference series, co-inventor of model checking and co-recipient (along with Edmund Clarke and Joseph Sifakis) of the 2007 ACM Turing Award, passed away on October 15th, 2024. The 2025 CAV conference program includes a E. Allen Emerson Memorial Symposium in his honor, offered as a full-day event on the first workshop day.
A direct off-spring of his dissertation work, Allen (together with his then PhD advisor, Edmund Clarke) developed the branching-time temporal logic CTL, as an alternative to the single-path linear-time logic LTL proposed by Amir Pnueli several years earlier. CTL lends itself beautifully to algorithmic decision procedures based on fixed-point theory, as shown in Allen’s 1980 ICALP paper with Edmund Clarke on “Characterizing Correctness Properties of Parallel Programs Using Fixpoints.” An algorithm for model checking transition systems against CTL properties was introduced in a paper in 1981, of a complexity linear in the size of the CTL formula. This paper also introduced the term model checking, almost as a historic accident: the paper was primarily about synthesizing concurrent systems.
Allen’s post-PhD work addressed many deep foundational aspects of the relationship between temporal logics, calculi, and automata and game theory. The mu-calculus, a rich language for formalizing logics (including CTL) that have fixed-point operators as their most powerful computational primitive, has an intricate relationship with alternating automata and infinite games. Allen’s work led to the concepts of parity games and parity automata, and paved the way to progress on determining the complexity of the mu-calculus model-checking problem.
In addition to the expressiveness of the logical formalism used to specify properties, another concern was the efficiency of the model checking procedure. Much of Allen’s later research, such as with his PhD students, was about one aspect or another of the state space explosion problem. Symmetry-based model reductions eliminate model redundancy inherent in systems of concurrent components with identical behavior descriptions, such as worker threads offering the same set of services for a large number of users of a cloud site. Parameterized verification attempts to verify properties over system families parameterized by the number of concurrently executing components or, in principle, any other parameterizable quantity.
A hallmark of Allen’s work was the depth to which he penetrated research problems, often spending many years (and several PhD students …) on finding answers to the most puzzling of questions. These questions were ever-present in his mind: An incautious remark, and you could easily get yourself caught up in a long discussion with him under impossible circumstances, such as at a busy Austin intersection when you and he were really supposed to part ways in different directions.
Short biography: Allen was born, and went to high school, in Dallas, Texas. He had an early interest in math and logic, and learned programming languages of the day, including BASIC, Fortran and Algol, many of them auto-didactically. He studied mathematics as an undergraduate at the University of Texas at Austin, graduating in 1976. His interest in computer science, however, prevailed, and he enrolled in Harvard University’s Applied Mathematics program—the closest to computer science available at Harvard at the time. He graduated in 1981 with a dissertation titled, “Branching Time Temporal Logic and the Design of Correct Concurrent Programs.” Shortly after his graduation, he became a full-time faculty member at his undergraduate Alma Mater, UT Austin, where he taught for about 35 years. Following his retirement in 2016, he stayed in touch with some of his former colleagues and many of his PhD students until his passing in 2024.