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 CAV conference has created a Memorial Page in his honor.
Allen made seminal contributions to the development of model checking, including work on efficient fixed point evaluation, symmetry-based reductions, and parameterized protocol verification. Allen's early research led to the invention of the branching-time temporal logics CTL and CTL*, along with efficient decision procedures for their satisfiability and model checking, as well as concurrent-program synthesis from CTL specifications. His keen interest in fixed-point logics resulted in groundbreaking mathematical discoveries that linked the mu-calculus with alternating automata and infinite games. This line of work introduced parity games and parity automata, and helped establish the complexity of mu-calculus model checking. The depth, breadth, and brilliance of Allen's work has influenced and inspired researchers worldwide.
We celebrate Allen's legacy with a day-long memorial symposium in his honor, to be held on July 21, 2025, as part of the first workshop day at CAV. The symposium is a place to hear about Allen's research and its impact, to talk about Allen as a collaborator, advisor, and friend, and simply to share stories of memorable interactions with him. The event will feature distinguished talks by leading researchers in formal methods and will include time for an open-mike session where audience members can share their own memories of Allen.
We hope that you will share with us your thoughts on Allen and his impact on you at the symposium. We will post the symposium program here shortly.
Kedar Namjoshi & Thomas Wahl
(Symposium co-organizers)