Dr. Paul A. G. Sivilotti
Associate Professor
Computer Science and Engineering
Site Navigation
CSE 788.P11 — Model Checking
Autumn 2006
| Instructor | Prof. Paul Sivilotti |
|---|---|
| Time/Place | M/W/F, 12:30 - 1:18, in DL 698 |
| Syllabus | See here |
| Newsgroup | cse.course.cse78811 |
| Credits | U G 3 (letter graded) |
| Grading | 80–100: A; 70–79: B; 60–69: C; 50–59: D; <50: E |
Contact Information
| Dr. Paul Sivilotti | |
|---|---|
paolo (at cse) |
|
| office | Dreese 695 |
| phone | 292-5835 |
| hours | Wed. 1:30 – 2:30 pm Fri. 9:30 – 10:30 am |
Course Description
The class will introduce some basic temporal logics, including CTL, LTL, and CTL*. Expressivity of these logics and issues of fairness will be discussed. We will cover Kripke structures and explicit state model checking. We will also cover BDDs and symbolic model checking. Students will work with model checkers of each kind. Additional topics, time permitting, could include: model checking LTL, compositional approaches to model checking, and optimization through abstraction and symmetry.
