Model checking is a technique increasingly used for validating software systems, especially systems with aspects of concurrency and real-time. Like its cousin formal verification, it is based on logic. However, unlike formal verification it does not require axiomatizations related to properties to be proven. Instead it attempt to exercise a model of the system exhaustively, treating it as a finite-state machine. Similarly, the temporal properties to be established are expressed in terms of finite-state machines on infinite sequences. Some very cool tools have been developed to checked these kinds of properties, and one will be demonstrated at the talk. This talk gives a brief introduction to model checking, and also serves as the trailer for a seminar course on the topic, which I am offering in Spring 2007.
HMC CS colloquium talks begin at 4:15pm sharp in Galileo Pryne on Thursdays. Prior to the talk, at 4:00pm, we have drinks and snacks in Hixon Court. Some talks will take place at Pomona College, in the same Thursday 4:15 p.m time-slot, but in the Rose Hills Theater in Pomona College's Smith Campus Center. These talks are considered part of our HMC colloquium series. (Sometimes Pomona College has talks at different times. Although you are encouraged to attend, these talks are not considered part of our colloquium series.)
| Date | Where | Speaker |
|---|---|---|
| 2006-08-31 | HMC, Pryne | Welcome Back |
| 2006-09-07 | HMC, Pryne | Nick Pippenger |
| 2006-09-14 | HMC, Pryne | A Software Tool for Learning Jazz Improvisation |
| 2006-09-21 | HMC, Pryne | Graduate-school Information Session |
| 2006-09-28 | HMC, Pryne | Optical Networking |
| 2006-10-05 | HMC, Pryne | Serge Belongie |
| 2006-10-12 | HMC, Pryne | LizardNet and TinkerNet |
| 2006-10-14 | Fall Break begins | |
| 2006-10-18 | Fall Break ends | |
| 2006-10-19 | Strategic Planning (No colloquium!) | |
| 2006-10-26 | PC, RHT | Kim Bruce |
| 2006-11-02 | HMC, Pryne | Spring-Semester Preview |
| 2006-11-09 | PC, RHT | Kathleen Fisher |
| 2006-11-16 | HMC, Pryne | Robert Keller |
| 2006-11-23 | Thanksgiving Break begins | |
| 2006-11-27 | Thanksgiving Break ends | |
| 2006-11-30 | PC, RHT | Yu-Han Chang |
| 2006-12-07 | HMC, Pryne | TBA (Student/Faculty Research or External Speaker)? |
| 2006-12-08 | Last day of Classes |
If you are a CS major, the Thursday 4:15–5:30pm time-slot belongs to CS Colloquium. An event is held every week at this time (sometimes at Pomona College).
You should plan on attending colloquium every week. To handle situations such as illness, Clinic site visits, forgetting to sign in, and so forth, you are allowed to miss three colloquia. Don't miss more than three! There is a sign-in sheet at every colloquium. Do not forget to sign it, otherwise we won't know that you attended. Do not sign for other people—doing so would violate the honor code.
When we have external speakers, there will be an after-colloquium dinner, to which students are invited on a first-come, first-served basis.