E. Allen Emerson

E. Allen Emerson (born 1954) is an American computer scientist and pioneer in the field of formal verification. He co-developed the symbolic model checking technique, which has had a transformative impact on verifying hardware and software systems for correctness. Emerson's work has been instrumental in advancing the field of formal methods in computer science.

Known for his work in formal methods, particularly in establishing program correctness. Inspired by papers and talks by Tony Hoare and Zohar Manna, Emerson co-invented and co-developed model checking, an algorithmic approach to verifying finite-state concurrent programs. His seminal paper with Ed Clarke in 1981 laid the foundations for the field of model checking. Emerson's contributions include advancements in model checking algorithms, abstractions, reductions, decision procedures, and program synthesis.

Ernest Allen Emerson II was an American computer scientist and winner of the 2007 Turing Award. He was a professor at the University of Texas at Austin from 1981 to 2016.

• Clarke and Joseph Sifakis for the invention and development of model checking, a technique used in formal verification of software and hardware.
• His contributions to temporal logic and modal logic include the introduction of computation tree logic (CTL) and its extension CTL*, which are used in the verification of concurrent systems.
• He is also recognized along with others for developing symbolic model checking to address combinatorial explosion that arises in many model checking algorithms.