E. Allen Emerson

E. Allen Emerson was an American computer scientist and professor at the University of Texas at Austin who, together with his doctoral advisor Edmund Clarke, helped invent model checking, a technique for automatically verifying that a hardware or software system satisfies a given specification. Emerson introduced computation tree logic and its extension CTL star as formal languages for expressing the properties model checking verifies, and he later developed symbolic model checking techniques to address the explosive growth in the number of states a real system can have. He shared the 2007 Turing Award with Clarke and Joseph Sifakis.