[See also CSE590K, Compiler Seminar, Spring 2000.]
The seminar meets in Loew 115, Mondays at 2:30 pm.
| Month | Day | Speaker | Title |
| April | 3 | Todd Millstein | Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications |
| April | 10 | Matthai Philipose | Symbolic Model Checking for Sequential Circuit Verification |
| April | 17 | Vivek Sahasranaman | Model Checking and Abstraction |
| April | 24 | Vass Litvinov | Program Analysis as Model Checking of Abstract Interpretations |
| May | 1 | Sorin Lerner | Data Flow Analysis as Model Checking |
| May | 8 | Mike Ernst | Bandera: Extracting Finite-State Models from Java Source Code |
| May | 15 | no meeting | |
| May | 22 | David Notkin | Model Checking Large Software Specifications |
| May | 29 | no meeting (Memorial Day) | |
| TBA | Tom Ball and Sriram Rajamani | Checking Temporal Properties of Software with Boolean Programs |