In Memoriam: E. Allen Emerson

E. Allen Emerson was the first graduate student of Edmund M. Clarke at Harvard University. After discussing several ideas for Allen's dissertation, they identified a promising candidate: verifying a finite-state system against a formal specification. According to Martha Clarke, Edmund's widow, it was during a walk across Harvard Yard that they decided to call it "model checking." Emerson received his Ph.D. in applied mathematics for this work in 1981. Twenty-five years later, he and Clarke (along with Joseph Sifakis) shared the ACM A.M. Turing Award in 2007 for this and related work.