This time table is tentative, and may be subject to change.

Tuesday lectures: 2pm-4pm, Ainsworth Building 201 (K-J17-201).

Thursday lectures: 1pm-2pm, The Michael Hintze Theatre (K-H6-LG03)

Week Dates Contents (tbc) Slides/Notes References
1 01/03
03/03
Introduction
Automata
Lecture 1
Lecture 2
Huth/Ryan $1, Sipser $1.1-1.2
Bayer/Katoen $2.1-2.2 (Parts)
2 08/03
10/03
Temporal Logics
Expressiveness
Lecture 3
Lecture 4
Huth/Ryan $3.2, $3.4, Bayer/Katoen $5.1,6.2 (Parts)
Huth/Ryan $3.5, Bayer/Katoen $6.3 (Parts)
3 15/03
17/03
CTL Model Checking
LTL and Büchi automata
Lecture 5
Lecture 6
Bérard et al. $3.1, Bayer/Katoen $6.4, Clarke et al. $4.1
Bayer/Katoen $5.2
4 22/03
24/03
 
LTL Model Checking
Tool: Spin
 
Lecture 7
Lecture 8
Spin: Examples
Bayer/Katoen $5.2
http://spinroot.com/;
http://spinroot.com/spin/Man/Quick.html
Mid-semester break (28 March to 1 April)
5 05/04
07/04
Static Analysis
Tool: Goanna
Lecture 9
Lecture 10
Nielsen/Nielsen/Hankin
 
6 12/04
14/04
Symbolic CTL Model Checking (1)
Binary Decision Diagrams
Lecture 11
Lecture 12
7 19/04
21/04
Symbolic CTL Model Checking (2)
Assignment 1
Lecture 13
 
8 26/04
28/04
Assignment 1, Tool: CBMC
Assignment 2
Lecture 14
Announcement
9 03/05
05/05
Abstraction Refinement (2)
Predicate Abstraction Refinement
Lecture 19
Lecture 20
10 10/05
12/05
Timed Automata
Region Graph
Lecture 21
Lecture 22
11 17/05
19/06
Timed Languages
Lecture 23
Lecture 24
12 24/05
26/06
Model Checking for Timed Automata
Real-time model checker: UPPAAL
Lecture 23
Lecture 24
13 31/05
 
Summary, Questions and Answers
(optional)
 


Copyright 2016