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 2025 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 2025. The Symposium is the 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 presentations and remarks by leading researchers in the field of formal verification, slides and videos documenting Allen's life in pictures, and an open-mike session where audience members can spontaneously share their own memories of Allen. The tentative Symposium program is as follows:
Participation in the Symposium requires registration for the first CAV workshop day; see the CAV registration page for full information. Complimentary lunch will be provided for all registered workshop participants.
We hope that you will share with us your thoughts on Allen and his impact on you at the Symposium.
Kedar Namjoshi & Thomas Wahl
(Symposium co-organizers)