Model Checking and Temporal Logic - E. Allen Emerson's Turing Award Lecture

Explore the life and work of E. Allen Emerson, the 2007 ACM Turing Award recipient, in this comprehensive interview. Delve into Emerson's early childhood, high school experiences, and family background before following his academic journey through college and his return to the University of Texas. Gain insights into his time at Harvard and the development of his interest in computer science, particularly in verification. Discover the state of the art in verification during Emerson's early career and learn about the invention of model checking, including the development of CTL and CTF. Understand the initial reception of model checking and its impact on the field of computer science. Examine the concepts of temporal logic, verification, and the debate between branching time and linear time approaches. This in-depth conversation provides a fascinating look at the career of a pioneering computer scientist and the evolution of crucial verification techniques in computing.

Introduction
Interview Structure
Turing Award citation
Early childhood
High school
Parents
College
College Years
Returning to UT
Visiting the Northeast
Wife
Harvard
Computer Science Education
Computer Science Courses
Interest in Verification
State of the Art in Verification
What is Model Checking
The Invention of Model Checking
CTL and CTF
Model checking
Rebranding a paper
Initial reception of model checking
Temporal logic
Verification
Branching Time vs Linear Time
Spinelli 77