Title: The Genesis and Development of Model Checking: Fact vs. Fiction
Speaker: Allen Emerson
Day: Wednesday, September 30
Clarke and Emerson are noted for the invention and development of model checking [CE81]. In this presentation, I will recall the roles of the principals. I was responsible for the initial conception of model checking, as a spinoff of my work on program synthesis. This entailed the checking of candidate models of a temporal specification algorithmically, and explains the coining of the term model checking. Model checking plainly was a form of verification circumventing proofs. As a part of some consulting work, Ed Clarke had been consulting on verification of protocols using temporal specifications and deductive proofs. As I discussed model checking with Ed, he envisioned that it could be a really practical verification method, applicable to protocols and more. Later, Ed commented that neither one of us could have achieved model checking without the other.
There are alternative perspectives on this history. In broad brush, these agree, but they vary in detail. I will elaborate with additional crucial facts, and examine their impact on various apparent discrepancies. I would like to suggest the relevance of Pnueli's Principle here: The junior researcher lives in the problem, while the senior researcher lives in a constant stream of interrupts. A Corollary is: The junior researcher will singlemindedly acquire a detailed memory concerning the problem and its solution; The overburdened, timesharing senior researcher will lack sufficient focused attention, blocks of time, and depth of understanding to have good recall.
[CE81] Edmund M. Clarke and E. Allen Emerson: Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. Logics of Programs, Workshop, Yorktown Heights, New York, May 1981