|
|
Model Checking Course Schedule |
Below is a list of lecture topics by date, as well as midterm, exam and project-due dates. The schedule is provisional and subject to change. Materials for each lecture, including slides and source code, are also available.
|
DATE |
TOPIC |
Project Milestones |
|
Th 01/26 |
Course intro |
|
|
Tu 01/31 |
Propositional logic: syntax and semantics |
|
|
Th 02/02 |
Satisfiability checking (SAT solving) |
|
|
Tu 02/07 |
The sequent calculus and proofs in propositional logic |
|
|
Th 02/09 |
Kripke structures and propositional linear temporal logic (LTL) |
|
|
Tu 02/14 |
Linear vs. branching time temporal logic: LTL, CTL, and CTL* |
|
|
Th 02/16 |
CTL model-checking via fixpoints |
|
|
Tu 02/21 |
CTL model checking (cont.) |
|
|
Th 02/23 |
CTL model checking and the nuSMV tool |
|
|
Tu 02/28 |
LTL and Buechi automata |
|
|
Th 03/02 |
LTL model checking via Buechi automata |
|
|
Tu 03/07 |
LTL model checking and the SPIN tool |
|
|
Th 03/09 |
Dealing with state explosion: bisimulation and minimization |
Project proposal
due |
|
Tu 03/14 |
Dealing with state
explosion: symbolic model checking |
|
|
Th 03/16 |
MIDTERM |
|
|
Tu 03/21 |
SPRING BREAK |
|
|
Th 03/23 |
SPRING BREAK |
|
|
Tu 03/28 |
Dealing with state
explosion: abstraction |
|
|
Th 03/30 |
Counter-example-guided
abstraction refinement (CEGAR) |
|
|
Tu 04/04 |
Timed automata and real-time systems |
|
|
Th 04/06 |
Model-checking
timed automata via proof search |
Project status
report due |
|
Tu 04/11 |
Proof search and
constraints |
|
|
Th 04/13 |
Predicate
calculus: syntax, semantics, sequent
calculus |
|
|
Tu 04/18 |
Satisfaction
modulo theories (SMT) solving and quantifier elimination |
|
|
Th 04/20 |
Timed automata
model checking and the UPPAAL tool |
|
|
Tu 04/25 |
Hybrid automata
and cyber-physical systems |
|
|
Th 04/27 |
Model checking hybrid automata |
|
|
Tu 05/02 |
Project presentations |
|
|
Th 05/04 |
Project presentations |
|
|
Tu 05/09 |
Project presentations |
|
|
Th 05/11 |
Project presentations |
|
|
F 05/19 |
FINAL (10:30 am – 12:30 pm) |
|