Program

All sessions will take place in Metropolitan A unless otherwise indicated.

Wednesday, August 16th

Wednesday's program is also available with abstracts or side by side with other meetings.

09:00‑10:30  Session

09:00	Edmund Clarke (Carnegie Mellon University) The Birth of Model Checking [ppt]
09:30	E. Allen Emerson (University of Texas, Austin) The Beginnings of Model Checking: A Personal Perspective
10:00	Bob Kurshan (Cadence Berkeley) 25 Years of Computer-Aided Verification [pdf]

10:30‑11:00  Break

11:00‑12:30  Session

11:00	Gerard Holzmann (NASA/JPL) New Challenges in Model Checking [pdf]
11:30	David Dill (Stanford University) A Retrospective on Murphi [ppt]
12:00	Rajeev Alur (University of Pennsylvania) Model Checking: From Tools to Theory [ppt]

12:30‑14:00  25MC Lunch/Panel
Chair: Orna Grumberg

12:30

The winners of the 1998 and 2006 ACM Kanellakis awards 25MC Lunch/Panel: Verification in the Next 25 Years

14:00‑15:30  Session

14:00	Thomas Henzinger (EPFL Lausanne & UC Berkeley) From Graph Models to Game Models [ppt]
14:30	Limor Fix (Intel Pittsburgh) Accelerating the Industrial Deployment of Model-Checking for SW Verification: Lessons from 10 years of Model-Checking Deployment for HW Verification in Intel [ppt]
15:00	Randy Bryant (Carnegie Mellon University) A View from the Engine Room: Computational Support for Symbolic Model Checking [ppt]

15:30‑16:00  Break

16:00‑17:30  Session

16:00	Ken McMillan (Cadence Berkeley) The Evolution of Symbolic Model Checking [ppt]
16:30	Moshe Y. Vardi (Rice University, Houston) From Church and Prior to PSL [pdf]
17:00	Amir Pnueli (Weizmann Institute and New York University) The Merits of Temporal Testers: Transducers Compose while Acceptors Do Not [pdf]