Ernest Allen Emerson II (June 2, 1954 – October 15, 2024) was an American computer scientist and winner of the 2007 Turing Award.

Emerson is recognized together with Edmund M. Clarke and Joseph Sifakis for the invention and development of model checking, a technique used in formal verification of software and hardware.

[1] In the early 1980s, Emerson and his PhD advisor, Edmund M. Clarke, developed techniques for verifying a finite-state system against a formal specification.

Emerson's work on model checking included early and influential temporal logics for describing specifications, and techniques for reducing state space explosion.

[1] The citation reads: for their role in developing Model-Checking into a highly effective verification technology that is widely adopted in the hardware and software industries.